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

end;

given B being Ordinal such that A6: ( B in A & x in Rank B ) ; :: thesis: x in Rank A
L . B = Rank B by A2, A6;
then Rank B in rng L by A2, A6, FUNCT_1:def 5;
hence x in Rank A by A3, A6, TARSKI:def 4; :: thesis: verum