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

proof

let y be object ; :: 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 object such that
A4: x in X and
A5: y = f . x by A1, FUNCT_1:def 3;
the_rank_of x in omega by A4, CLASSES1:66;
hence y in NAT by A2, A4, A5; :: thesis: verum

end;

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

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

then the_rank_of X = 0 by CLASSES1:71;
hence X in Rank omega by CLASSES1:66; :: 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:8, RELAT_1:42;
reconsider mY = max Y as Element of NAT by ORDINAL1:def 12;
set i = 1 + mY;
X c= Rank (1 + mY)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank (1 + mY) )
reconsider xx = x as set by TARSKI:1;
assume A6: x in X ; :: thesis: x in Rank (1 + mY)
then A7: f . x in Y by A1, FUNCT_1:def 3;
A8: f . x = the_rank_of xx by A2, A6;
reconsider j = f . x as Element of NAT by A7;
j <= mY by A7, XXREAL_2:def 8;
then Segm j c= Segm mY by NAT_1:39;
then A9: j in succ mY by ORDINAL1:22;
succ (Segm mY) = Segm (1 + mY) by NAT_1:38;
hence x in Rank (1 + mY) by A8, A9, CLASSES1:66; :: thesis: verum

end;

then the_rank_of X c= 1 + mY by CLASSES1:65;
then A10: the_rank_of X in succ (1 + mY) by ORDINAL1:22;
Segm ((1 + mY) + 1) = succ (Segm (1 + mY)) by NAT_1:38;
hence X in Rank omega by A10, CLASSES1:66; :: thesis: verum

end;

end;