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 x in bool X ; :: thesis: x in Rank (succ A)
then ( x c= Rank A & Rank (succ A) = bool (Rank A) ) by A1, Lm2, XBOOLE_1:1;
hence x in Rank (succ A) ; :: thesis: verum

end;

assume A2: 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 x in X ; :: thesis: x in Rank A
then {x} c= X by ZFMISC_1:37;
then ( {x} in bool X & Rank (succ A) = bool (Rank A) ) by Lm2;
then ( {x} c= Rank A & x in {x} ) by A2, TARSKI:def 1;
hence x in Rank A ; :: thesis: verum