let A be Ordinal; :: thesis: Rank A c= Rank (succ A)
A1: Rank A in bool (Rank A) by ZFMISC_1:def 1;
A2: Rank A in Rank (succ A) by A1, Lm2;
thus Rank A c= Rank (succ A) by A2, ORDINAL1:def 2; :: thesis: verum