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 A3: x in bool X ; :: thesis: x in Rank (succ (the_rank_of X))
A4: x c= Rank (the_rank_of X) by A1, A3, XBOOLE_1:1;
A5: bool (Rank (the_rank_of X)) = Rank (succ (the_rank_of X)) by Lm2;
thus x in Rank (succ (the_rank_of X)) by A4, A5; :: thesis: verum

end;

A6: 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;
A9: ex A being Ordinal st S₁[A] by A7, A8;
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);

A11: now

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

end;

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

end;

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