let A be Ordinal; :: thesis: Rank A c= Rank (succ A)
Rank A in bool (Rank A) by ZFMISC_1:def 1;
then Rank A in Rank (succ A) by Lm2;
hence Rank A c= Rank (succ A) by ORDINAL1:def 2; :: thesis: verum