let X be set ; :: thesis: the_rank_of (bool X) = succ (the_rank_of X)
A1: X c= Rank (the_rank_of X) by Def9;
A2: bool X c= Rank (succ (the_rank_of X))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in Rank (succ (the_rank_of X)) )
reconsider xx = x as set by TARSKI:1;
assume x in bool X ; :: thesis: x in Rank (succ (the_rank_of X))
then A3: xx c= Rank (the_rank_of X) by A1;
bool (Rank (the_rank_of X)) = Rank (succ (the_rank_of X)) by Lm2;
hence x in Rank (succ (the_rank_of X)) by A3; :: thesis: verum

end;

for A being Ordinal st bool X c= Rank A holds
succ (the_rank_of X) c= A

proof

let A be Ordinal; :: thesis: ( bool X c= Rank A implies succ (the_rank_of X) c= A )
assume A4: bool X c= Rank A ; :: thesis: succ (the_rank_of X) c= A
defpred S₁[ Ordinal] means X in Rank $1;
A5: X in bool X by ZFMISC_1:def 1;
then A6: ex A being Ordinal st S₁[A] by A4;
consider B being Ordinal such that
A7: ( S₁[B] & ( for C being Ordinal st S₁[C] holds
B c= C ) ) from ORDINAL1:sch 1(A6);

now :: thesis: not for C being Ordinal holds B <> succ C

assume for C being Ordinal holds B <> succ C ; :: thesis: contradiction
then B is limit_ordinal by ORDINAL1:29;
then ex C being Ordinal st
( C in B & X in Rank C ) by A7, Lm2, Th31;
hence contradiction by A7, ORDINAL1:5; :: thesis: verum

end;

then consider C being Ordinal such that
A8: B = succ C ;
X c= Rank C by A7, A8, Th32;
then the_rank_of X c= C by Def9;
then A9: the_rank_of X in B by A8, ORDINAL1:22;
B c= A by A4, A5, A7;
hence succ (the_rank_of X) c= A by A9, ORDINAL1:21; :: thesis: verum

end;

hence the_rank_of (bool X) = succ (the_rank_of X) by A2, Def9; :: thesis: verum