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

end;

assume X in Rank (succ A) ; :: thesis: X c= Rank A
then X in bool (Rank A) by Lm2;
hence X c= Rank A ; :: thesis: verum