defpred S1[ set , set ] means $2 c= $1;
assume A1: cf omega <> omega ; :: thesis: contradiction
cf omega c= omega by Def1;
then cf omega in omega by A1, CARD_1:3;
then reconsider B = cf omega as finite set ;
set n = card B;
A2: for x, y being set st S1[x,y] & S1[y,x] holds
x = y ;
A3: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] by XBOOLE_1:1;
omega is_cofinal_with card B by Def1;
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 ;
reconsider rxi = rng xi as finite set by A4, FINSET_1:8;
A7: rxi <> {} by A6, ORDINAL2:18;
consider x being set such that
A8: ( x in rxi & ( for y being set st y in rxi & y <> x holds
not S1[y,x] ) ) from CARD_2:sch 3(A7, A2, A3);
 reconsider x = x as Ordinal by A5, A8;
now :: thesis: for A being Ordinal st A in rng xi holds
A in succ x
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:22; :: thesis: verum
end;
then A9: omega c= succ x by A6, ORDINAL2:20;
succ x in omega by A5, A8, ORDINAL1:28;
hence contradiction by A9; :: thesis: verum