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

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 A8;
hence A in succ x by ORDINAL1:34; :: thesis: verum

end;

then A9: omega c= succ x by A6, ORDINAL2:28;
succ x in omega by A5, A8, ORDINAL1:41;
hence contradiction by A9, ORDINAL1:7; :: thesis: verum