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

proof

assume A1: X c= Rank A ; :: thesis: bool X c= Rank (succ A)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in Rank (succ A) )
assume A2: x in bool X ; :: thesis: x in Rank (succ A)
A3: x c= Rank A by A1, A2, XBOOLE_1:1;
A4: Rank (succ A) = bool (Rank A) by Lm2;
thus x in Rank (succ A) by A3, A4; :: thesis: verum

end;

assume A5: bool X c= Rank (succ A) ; :: thesis: X c= Rank A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank A )
assume A6: x in X ; :: thesis: x in Rank A
A7: {x} c= X by A6, ZFMISC_1:37;
A8: {x} in bool X by A7;
A9: ( Rank (succ A) = bool (Rank A) & x in {x} ) by Lm2, TARSKI:def 1;
thus x in Rank A by A5, A8, A9; :: thesis: verum