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 ( bool X c= Rank A & the_rank_of (bool X) = succ (the_rank_of X) ) by Th36, Th71;
then ( the_rank_of X in the_rank_of (bool X) & the_rank_of (bool X) c= A ) by Def8, ORDINAL1:10;
hence the_rank_of X in A ; :: thesis: verum

end;

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