thus aleph 0 c= omega by Lm1, Th7; :: according to XBOOLE_0:def 10 :: thesis: omega c= aleph 0
thus omega c= aleph 0 :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in omega or x in aleph 0 )
assume A1: x in omega ; :: thesis: x in aleph 0
then reconsider A = x as Ordinal ;
consider n being Element of omega such that
A2: A = n by A1;
card (succ n) c= card omega by Th10, ORDINAL1:21;
hence x in aleph 0 by A2, Lm1, ORDINAL1:6; :: thesis: verum
end;