assume A1: cf omega <> omega ; :: thesis: contradiction
cf omega c= omega by Def2;
then cf omega in omega by A1, CARD_1:13;
then reconsider B = cf omega as finite set ;
set n = card B;
( card (cf omega ) = cf omega & card B = card (card B) & card (cf omega ) = card (card B) ) by CARD_1:def 5;
then omega is_cofinal_with card B by Def2;
then consider xi being Ordinal-Sequence such that
A2: ( dom xi = card B & rng xi c= omega & xi is increasing & omega = sup xi ) by ORDINAL2:def 21;
reconsider rxi = rng xi as finite set by A2, FINSET_1:26;
defpred S₁[ set , set ] means $2 c= $1;
A3: rxi <> {} by A2, ORDINAL2:26;
A4: for x, y being set st S₁[x,y] & S₁[y,x] holds
x = y by XBOOLE_0:def 10;
A5: for x, y, z being set st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by XBOOLE_1:1;
consider x being set such that
A6: ( x in rxi & ( for y being set st y in rxi & y <> x holds
not S₁[y,x] ) ) from CARD_3:sch 2(A3, A4, A5);
reconsider x = x as Ordinal by A2, A6;

now

let A be Ordinal; :: thesis: ( A in rng xi implies A in succ x )
assume A in rng xi ; :: thesis: A in succ x
then ( A c= x or not x c= A ) by A6;
hence A in succ x by ORDINAL1:34; :: thesis: verum

end;

then ( omega c= succ x & succ x in omega ) by A2, A6, ORDINAL1:41, ORDINAL2:28;
hence contradiction by ORDINAL1:7; :: thesis: verum