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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in Rank A )
assume x in bool X ; :: thesis: x in Rank A
hence x in Rank A by A1, Th47; :: thesis: verum

end;

hence bool X in Rank (succ A) by Th36; :: 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 Th36, ZFMISC_1:def 1;
hence X in Rank A ; :: thesis: verum