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) 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 A3: Y in X ; :: thesis: the_rank_of Y in A
A4: Y in Rank (the_rank_of X) by A1, A3;
A5: Rank (the_rank_of X) c= Rank A by A2, Th43;
thus the_rank_of Y in A by A4, A5, Th74; :: thesis: verum

end;

assume A6: for Y being set st Y in X holds
the_rank_of Y in A ; :: thesis: the_rank_of X c= A
A7: 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 A8: x in X ; :: thesis: x in Rank A
A9: the_rank_of x in A by A6, A8;
thus x in Rank A by A9, Th74; :: thesis: verum

end;

thus the_rank_of X c= A by A7, Def8; :: thesis: verum