thus alef 0 c= omega by Lm1, Th24; :: according to XBOOLE_0:def 10 :: thesis: omega c= alef 0
thus omega c= alef 0 :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in omega or x in alef 0 )
assume A1: x in omega ; :: thesis: x in alef 0
then reconsider A = x as Ordinal ;
consider n being Element of omega such that
A2: A = n by A1;
succ n c= omega by ORDINAL1:33;
then ( card (succ n) c= card omega & n in succ n & card (succ n) = succ n ) by Def5, Th27, ORDINAL1:10;
hence x in alef 0 by A2, Lm1; :: thesis: verum

end;