thus for X, Y being set st X in Rank omega & Y c= X holds
Y in Rank omega by CLASSES1:47; :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( ( for b1 being set holds
( not b1 in Rank omega or bool b1 in Rank omega ) ) & ( for b1 being set holds
( not b1 c= Rank omega or b1, Rank omega are_equipotent or b1 in Rank omega ) ) )
thus for X being set st X in Rank omega holds
bool X in Rank omega :: thesis: for b1 being set holds
( not b1 c= Rank omega or b1, Rank omega are_equipotent or b1 in Rank omega )
proof
let X be set ; :: thesis: ( X in Rank omega implies bool X in Rank omega )
assume X in Rank omega ; :: thesis: bool X in Rank omega
then consider A being Ordinal such that
A1: ( A in omega & X in Rank A ) by Lm5, CLASSES1:35;
( succ A in omega & bool X in Rank (succ A) ) by A1, Lm5, CLASSES1:48, ORDINAL1:41;
hence bool X in Rank omega by Lm5, CLASSES1:35; :: thesis: verum
end;
thus for X being set holds
( not X c= Rank omega or X, Rank omega are_equipotent or X in Rank omega ) :: thesis: verum
proof
let X be set ; :: thesis: ( not X c= Rank omega or X, Rank omega are_equipotent or X in Rank omega )
assume A2: ( X c= Rank omega & not X, Rank omega are_equipotent & not X in Rank omega ) ; :: thesis: contradiction
then ( card X c= card omega & card X <> card omega ) by Th69, CARD_1:21, CARD_1:27;
then ( card X = card X & card X in omega ) by CARD_1:13, CARD_1:84;
then consider n being Element of NAT such that
A3: n = card X ;
A4: ( card X = card n & omega c= Rank omega ) by A3, CLASSES1:44;
( X,n are_equipotent & n is finite ) by A3, CARD_1:def 5;
then reconsider X = X as finite set by CARD_1:68;
defpred S2[ set , set ] means the_rank_of $2 c= the_rank_of $1;
0 in omega ;
then A5: X <> {} by A2, A4;
A6: for x, y being set holds
( S2[x,y] or S2[y,x] ) ;
A7: for x, y, z being set st S2[x,y] & S2[y,z] holds
S2[x,z] by XBOOLE_1:1;
consider x being set such that
A8: ( x in X & ( for y being set st y in X holds
S2[x,y] ) ) from CARD_3:sch 3(A5, A6, A7);
 set A = the_rank_of x;
now
let Y be set ; :: thesis: ( Y in X implies the_rank_of Y in succ (the_rank_of x) )
assume Y in X ; :: thesis: the_rank_of Y in succ (the_rank_of x)
then ( the_rank_of Y c= the_rank_of x & Y = Y ) by A8;
hence the_rank_of Y in succ (the_rank_of x) by ORDINAL1:34; :: thesis: verum
end;
then A9: the_rank_of X c= succ (the_rank_of x) by CLASSES1:77;
the_rank_of x in omega by A2, A8, CLASSES1:74;
then succ (the_rank_of x) in omega by Lm5, ORDINAL1:41;
then the_rank_of X in omega by A9, ORDINAL1:22;
hence contradiction by A2, CLASSES1:74; :: thesis: verum
end;