let X be finite Subset of (Rank omega ); :: thesis: X in Rank omega
deffunc H₂( set ) -> set = the_rank_of $1;
consider f being Function such that
A1: dom f = X and
A2: for x being set st x in X holds
f . x = H₂(x) from FUNCT_1:sch 3();
A3: rng f c= NAT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then consider x being set such that
A4: ( x in X & y = f . x ) by A1, FUNCT_1:def 5;
the_rank_of x in omega by A4, CLASSES1:74;
hence y in NAT by A2, A4; :: thesis: verum

end;

per cases ( X = {} or X <> {} ) ;

suppose X = {} ; :: thesis: X in Rank omega

then ( the_rank_of X = {} & {} in omega & omega is ordinal ) by CLASSES1:79;
hence X in Rank omega by CLASSES1:74; :: thesis: verum

end;

suppose X <> {} ; :: thesis: X in Rank omega

then reconsider Y = rng f as non empty finite Subset of NAT by A1, A3, FINSET_1:26, RELAT_1:65;
reconsider mY = max Y as Element of NAT by ORDINAL1:def 13;
set i = 1 + mY;
X c= Rank (1 + mY)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank (1 + mY) )
assume x in X ; :: thesis: x in Rank (1 + mY)
then A5: ( f . x in Y & f . x = the_rank_of x ) by A1, A2, FUNCT_1:def 5;
then reconsider j = f . x as Element of NAT ;
j <= mY by A5, XXREAL_2:def 8;
then j c= mY by NAT_1:40;
then j in succ mY by ORDINAL1:34;
then ( succ j c= succ mY & succ mY = 1 + mY & j in succ j ) by NAT_1:39, ORDINAL1:33;
hence x in Rank (1 + mY) by A5, CLASSES1:74; :: thesis: verum

end;

then the_rank_of X c= 1 + mY by CLASSES1:73;
then ( the_rank_of X in succ (1 + mY) & (1 + mY) + 1 c= omega & (1 + mY) + 1 = succ (1 + mY) ) by NAT_1:39, ORDINAL1:34;
hence X in Rank omega by CLASSES1:74; :: thesis: verum

end;

end;