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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in Rank (succ A) )
reconsider xx = x as set by TARSKI:1;
assume x in bool X ; :: thesis: x in Rank (succ A)
then A2: xx c= Rank A by A1;
Rank (succ A) = bool (Rank A) by Lm2;
hence x in Rank (succ A) by A2; :: thesis: verum

end;

assume A3: bool X c= Rank (succ A) ; :: thesis: X c= Rank A
let x be object ; :: 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:31;
then A4: {x} in bool X ;
( Rank (succ A) = bool (Rank A) & x in {x} ) by Lm2, TARSKI:def 1;
hence x in Rank A by A3, A4; :: thesis: verum