let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal implies for x being set holds
( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) ) )
assume A1: ( A <> {} & A is limit_ordinal ) ; :: thesis: for x being set holds
( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) )
consider L being Sequence such that
A2: ( dom L = A & ( for B being Ordinal st B in A holds
L . B = H₁(B) ) ) from ORDINAL2:sch 2();
A3: Rank A = union (rng L) by A1, A2, Lm2;
let x be set ; :: thesis: ( x in Rank A iff ex B being Ordinal st
( B in A & x in Rank B ) )
thus ( x in Rank A implies ex B being Ordinal st
( B in A & x in Rank B ) ) :: thesis: ( ex B being Ordinal st
( B in A & x in Rank B ) implies x in Rank A )

proof

assume x in Rank A ; :: thesis: ex B being Ordinal st
( B in A & x in Rank B )
then consider Y being set such that
A4: x in Y and
A5: Y in rng L by A3, TARSKI:def 4;
consider y being object such that
A6: y in dom L and
A7: Y = L . y by A5, FUNCT_1:def 3;
reconsider y = y as Ordinal by A6;
take y ; :: thesis: ( y in A & x in Rank y )
thus ( y in A & x in Rank y ) by A2, A4, A6, A7; :: thesis: verum

end;

given B being Ordinal such that A8: B in A and
A9: x in Rank B ; :: thesis: x in Rank A
L . B = Rank B by A2, A8;
then Rank B in rng L by A2, A8, FUNCT_1:def 3;
hence x in Rank A by A3, A9, TARSKI:def 4; :: thesis: verum