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 Th42;
then A1: bool X c= Rank A by Th32;
the_rank_of (bool X) = succ (the_rank_of X) by Th63;
then A2: the_rank_of X in the_rank_of (bool X) by ORDINAL1:6;
the_rank_of (bool X) c= A by A1, Def9;
hence the_rank_of X in A by A2; :: thesis: verum
end;
assume A3: the_rank_of X in A ; :: thesis: X in Rank A
X c= Rank (the_rank_of X) by Def9;
then A4: X in Rank (succ (the_rank_of X)) by Th32;
Rank (succ (the_rank_of X)) c= Rank A by A3, Th37, ORDINAL1:21;
hence X in Rank A by A4; :: thesis: verum