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)
A2: 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 A3: x in bool X ; :: thesis: x in Rank A
thus x in Rank A by A1, A3, Th47; :: thesis: verum

end;

thus bool X in Rank (succ A) by A2, Th36; :: thesis: verum

end;

assume A4: bool X in Rank (succ A) ; :: thesis: X in Rank A
A5: ( X in bool X & bool X c= Rank A ) by A4, Th36, ZFMISC_1:def 1;
thus X in Rank A by A5; :: thesis: verum