let X be set ; :: thesis: for A being Ordinal holds
( X in Rank A iff the_rank_of X in A )
let A be Ordinal; :: thesis: ( X in Rank A iff the_rank_of X in A )
thus ( X in Rank A implies the_rank_of X in A ) :: thesis: ( the_rank_of X in A implies X in Rank A )

proof

assume X in Rank A ; :: thesis: the_rank_of X in A
then bool X in Rank (succ A) by Th48;
then A3: bool X c= Rank A by Th36;
the_rank_of (bool X) = succ (the_rank_of X) by Th71;
then A5: the_rank_of X in the_rank_of (bool X) by ORDINAL1:10;
the_rank_of (bool X) c= A by A3, Def8;
hence the_rank_of X in A by A5; :: thesis: verum

end;

assume the_rank_of X in A ; :: thesis: X in Rank A
then A8: succ (the_rank_of X) c= A by ORDINAL1:33;
X c= Rank (the_rank_of X) by Def8;
then A10: X in Rank (succ (the_rank_of X)) by Th36;
Rank (succ (the_rank_of X)) c= Rank A by A8, Th43;
hence X in Rank A by A10; :: thesis: verum