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

proof

assume A1: X in Rank A ; :: thesis: bool X in Rank (succ A)
bool X c= Rank A by A1, Th41;
hence bool X in Rank (succ A) by Th32; :: thesis: verum

end;

assume bool X in Rank (succ A) ; :: thesis: X in Rank A
then ( X in bool X & bool X c= Rank A ) by Th32, ZFMISC_1:def 1;
hence X in Rank A ; :: thesis: verum