begin
theorem
for
a,
b being ( ( ) ( )
set ) st
a : ( ( ) ( )
set )
in b : ( ( ) ( )
set ) holds
a : ( ( ) ( )
set ) is ( ( ) ( )
Element of
b : ( ( ) ( )
set ) ) ;
theorem
for
a,
b being ( ( ) ( )
set ) st
a : ( ( ) ( )
set ) is ( ( ) ( )
Element of
b : ( ( ) ( )
set ) ) & not
b : ( ( ) ( )
set ) is
empty holds
a : ( ( ) ( )
set )
in b : ( ( ) ( )
set ) ;
theorem
for
a,
b being ( ( ) ( )
set ) holds
(
a : ( ( ) ( )
set ) is ( ( ) ( )
Subset of ( ( ) ( non
empty )
set ) ) iff
a : ( ( ) ( )
set )
c= b : ( ( ) ( )
set ) ) ;
theorem
for
a,
b,
c being ( ( ) ( )
set ) st
a : ( ( ) ( )
set )
in b : ( ( ) ( )
set ) &
b : ( ( ) ( )
set ) is ( ( ) ( )
Subset of ( ( ) ( non
empty )
set ) ) holds
a : ( ( ) ( )
set ) is ( ( ) ( )
Element of
c : ( ( ) ( )
set ) ) ;
theorem
for
a,
b,
c being ( ( ) ( )
set ) st
a : ( ( ) ( )
set )
in b : ( ( ) ( )
set ) &
b : ( ( ) ( )
set ) is ( ( ) ( )
Subset of ( ( ) ( non
empty )
set ) ) holds
not
c : ( ( ) ( )
set ) is
empty ;