let X be set ; :: thesis: for A being Ordinal holds
( A c= the_rank_of X iff for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) )
let A be Ordinal; :: thesis: ( A c= the_rank_of X iff for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) )
thus ( A c= the_rank_of X implies for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ) :: thesis: ( ( for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ) implies A c= the_rank_of X )

proof

assume A1: A c= the_rank_of X ; :: thesis: for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y )
let B be Ordinal; :: thesis: ( B in A implies ex Y being set st
( Y in X & B c= the_rank_of Y ) )
assume B in A ; :: thesis: ex Y being set st
( Y in X & B c= the_rank_of Y )
then not the_rank_of X c= B by A1, ORDINAL1:7;
then not X c= Rank B by Def8;
then A5: X \ (Rank B) <> {} by XBOOLE_1:37;
consider x being Element of X \ (Rank B);
take x ; :: thesis: ( x in X & B c= the_rank_of x )
A6: not x in Rank B by A5, XBOOLE_0:def 5;
thus x in X by A5, XBOOLE_0:def 5; :: thesis: B c= the_rank_of x
not the_rank_of x in B by A6, Th74;
hence B c= the_rank_of x by ORDINAL1:26; :: thesis: verum

end;

assume A8: for B being Ordinal st B in A holds
ex Y being set st
( Y in X & B c= the_rank_of Y ) ; :: thesis: A c= the_rank_of X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the_rank_of X )
assume A9: x in A ; :: thesis: x in the_rank_of X
then reconsider x = x as Ordinal ;
consider Y being set such that
A10: Y in X and
A11: x c= the_rank_of Y by A8, A9;
the_rank_of Y in the_rank_of X by A10, Th76;
hence x in the_rank_of X by A11, ORDINAL1:22; :: thesis: verum