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

proof

assume A2: the_rank_of X c= A ; :: thesis: for Y being set st Y in X holds
the_rank_of Y in A
let Y be set ; :: thesis: ( Y in X implies the_rank_of Y in A )
assume Y in X ; :: thesis: the_rank_of Y in A
then ( Y in Rank (the_rank_of X) & Rank (the_rank_of X) c= Rank A ) by A1, A2, Th43;
hence the_rank_of Y in A by Th74; :: thesis: verum

end;

assume A3: for Y being set st Y in X holds
the_rank_of Y in A ; :: thesis: the_rank_of X c= A
X c= Rank A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank A )
assume x in X ; :: thesis: x in Rank A
then the_rank_of x in A by A3;
hence x in Rank A by Th74; :: thesis: verum

end;

hence the_rank_of X c= A by Def8; :: thesis: verum