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 T-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 A4: x in Rank A ; :: thesis: ex B being Ordinal st
( B in A & x in Rank B )
consider Y being set such that
A5: x in Y and
A6: Y in rng L by A3, A4, TARSKI:def 4;
consider y being set such that
A7: y in dom L and
A8: Y = L . y by A6, FUNCT_1:def 5;
reconsider y = y as Ordinal by A7;
take y ; :: thesis: ( y in A & x in Rank y )
thus ( y in A & x in Rank y ) by A2, A5, A7, A8; :: thesis: verum

end;

given B being Ordinal such that A9: B in A and
A10: x in Rank B ; :: thesis: x in Rank A
A11: L . B = Rank B by A2, A9;
A12: Rank B in rng L by A2, A9, A11, FUNCT_1:def 5;
thus x in Rank A by A3, A10, A12, TARSKI:def 4; :: thesis: verum