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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in Rank (succ (the_rank_of X)) )
assume x in bool X ; :: thesis: x in Rank (succ (the_rank_of X))
then A4: x c= Rank (the_rank_of X) by A1, XBOOLE_1:1;
bool (Rank (the_rank_of X)) = Rank (succ (the_rank_of X)) by Lm2;
hence x in Rank (succ (the_rank_of X)) by A4; :: 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 A7: bool X c= Rank A ; :: thesis: succ (the_rank_of X) c= A
defpred S₁[ Ordinal] means X in Rank $1;
A8: X in bool X by ZFMISC_1:def 1;
then A9: ex A being Ordinal st S₁[A] by A7;
consider B being Ordinal such that
A10: ( S₁[B] & ( for C being Ordinal st S₁[C] holds
B c= C ) ) from ORDINAL1:sch 1(A9);

now

assume for C being Ordinal holds B <> succ C ; :: thesis: contradiction
then B is limit_ordinal by ORDINAL1:42;
then ex C being Ordinal st
( C in B & X in Rank C ) by A10, Lm2, Th35;
hence contradiction by A10, ORDINAL1:7; :: thesis: verum

end;

then consider C being Ordinal such that
A15: B = succ C ;
X c= Rank C by A10, A15, Th36;
then the_rank_of X c= C by Def8;
then A18: the_rank_of X in B by A15, ORDINAL1:34;
B c= A by A7, A8, A10;
hence succ (the_rank_of X) c= A by A18, ORDINAL1:33; :: thesis: verum

end;

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