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

proof

assume A1: X c= Rank A ; :: thesis: X in Rank (succ A)
A2: X in bool (Rank A) by A1;
thus X in Rank (succ A) by A2, Lm2; :: thesis: verum

end;

assume A3: X in Rank (succ A) ; :: thesis: X c= Rank A
A4: X in bool (Rank A) by A3, Lm2;
thus X c= Rank A by A4; :: thesis: verum