thus for X, Y being set st X in Rank omega & Y c= X holds
Y in Rank omega by CLASSES1:41; :: 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 and
A2: X in Rank A by Lm5, CLASSES1:31;
A3: bool X in Rank (succ A) by A2, CLASSES1:42;
succ A in omega by A1, Lm5, ORDINAL1:28;
hence bool X in Rank omega by A3, Lm5, CLASSES1:31; :: 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 )
A4: 0 in omega ;
defpred S2[ object , object ] means the_rank_of $2 c= the_rank_of $1;
assume that
A5: X c= Rank omega and
A6: not X, Rank omega are_equipotent and
A7: not X in Rank omega ; :: thesis: contradiction
A8: card X <> card omega by A6, Th62, CARD_1:5;
card X c= card omega by A5, Th62, CARD_1:11;
then card X in omega by A8, CARD_1:3;
then reconsider X = X as finite set ;
A9: for x, y being object holds
( S2[x,y] or S2[y,x] ) ;
A10: for x, y, z being object st S2[x,y] & S2[y,z] holds
S2[x,z] by XBOOLE_1:1;
omega c= Rank omega by CLASSES1:38;
then A11: X <> {} by A7, A4;
consider x being object such that
A12: ( x in X & ( for y being object st y in X holds
S2[x,y] ) ) from CARD_2:sch 2(A11, A9, A10);
 set A = the_rank_of x;
for Y being set st Y in X holds
the_rank_of Y in succ (the_rank_of x) by A12, ORDINAL1:22;
then A13: the_rank_of X c= succ (the_rank_of x) by CLASSES1:69;
the_rank_of x in omega by A5, A12, CLASSES1:66;
then succ (the_rank_of x) in omega by Lm5, ORDINAL1:28;
then the_rank_of X in omega by A13, ORDINAL1:12;
hence contradiction by A7, CLASSES1:66; :: thesis: verum
end;