begin
theorem
for
X being ( ( ) ( )
set ) holds
X : ( ( ) ( )
set )
\/ {} : ( ( ) ( )
set ) : ( ( ) ( )
set )
= X : ( ( ) ( )
set ) ;
theorem
for
X being ( ( ) ( )
set ) holds
X : ( ( ) ( )
set )
/\ {} : ( ( ) ( )
set ) : ( ( ) ( )
set )
= {} : ( ( ) ( )
set ) ;
theorem
for
X being ( ( ) ( )
set ) holds
X : ( ( ) ( )
set )
\ {} : ( ( ) ( )
set ) : ( ( ) ( )
set )
= X : ( ( ) ( )
set ) ;
theorem
for
X being ( ( ) ( )
set ) holds
{} : ( ( ) ( )
set )
\ X : ( ( ) ( )
set ) : ( ( ) ( )
set )
= {} : ( ( ) ( )
set ) ;
theorem
for
X being ( ( ) ( )
set ) holds
X : ( ( ) ( )
set )
\+\ {} : ( ( ) ( )
set ) : ( ( ) ( )
set )
= X : ( ( ) ( )
set ) ;
theorem
for
X being ( ( ) ( )
set ) st
X : ( ( ) ( )
set ) is
empty holds
X : ( ( ) ( )
set )
= {} : ( ( ) ( )
set ) ;
theorem
for
x,
X being ( ( ) ( )
set ) st
x : ( ( ) ( )
set )
in X : ( ( ) ( )
set ) holds
not
X : ( ( ) ( )
set ) is
empty ;
theorem
for
X,
Y being ( ( ) ( )
set ) st
X : ( ( ) ( )
set ) is
empty &
X : ( ( ) ( )
set )
<> Y : ( ( ) ( )
set ) holds
not
Y : ( ( ) ( )
set ) is
empty ;