set Y = { x where x is Element of X : x is atom } ;
A1: now :: thesis: for y being object st y in { x where x is Element of X : x is atom } holds
y in the carrier of X
let y be object ; :: thesis: ( y in { x where x is Element of X : x is atom } implies y in the carrier of X )
assume y in { x where x is Element of X : x is atom } ; :: thesis: y in the carrier of X
then ex x being Element of X st
( y = x & x is atom ) ;
hence y in the carrier of X ; :: thesis: verum
end;
for z being Element of X st z \ (0. X) = 0. X holds
z = 0. X by Th2;
then 0. X is atom ;
then 0. X in { x where x is Element of X : x is atom } ;
hence { x where x is Element of X : x is atom } is non empty Subset of X by A1, TARSKI:def 3; :: thesis: verum