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:21;
then A3: card (succ n) c= card omega by Th27;
( n in succ n & card (succ n) = succ n ) by Def5, ORDINAL1:6;
hence x in alef 0 by A2, A3, Lm1; :: thesis: verum

end;