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 A1: X in Rank A ; :: thesis: the_rank_of X in A
A2: bool X in Rank (succ A) by A1, Th48;
A3: bool X c= Rank A by A2, Th36;
A4: the_rank_of (bool X) = succ (the_rank_of X) by Th71;
A5: the_rank_of X in the_rank_of (bool X) by A4, ORDINAL1:10;
A6: the_rank_of (bool X) c= A by A3, Def8;
thus the_rank_of X in A by A5, A6; :: thesis: verum

end;

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