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

now

assume for C being Ordinal holds B <> succ C ; :: thesis: contradiction
then B is limit_ordinal by ORDINAL1:42;
then consider C being Ordinal such that
A7: ( C in B & X in Rank C ) by A6, Lm2, Th35;
thus contradiction by A6, A7, ORDINAL1:7; :: thesis: verum

end;

then consider C being Ordinal such that
A8: B = succ C ;
X c= Rank C by A6, A8, Th36;
then the_rank_of X c= C by Def8;
then the_rank_of X in B by A8, ORDINAL1:34;
then ( succ (the_rank_of X) c= B & B c= A ) by A3, A4, A6, ORDINAL1:33;
hence succ (the_rank_of X) c= A by XBOOLE_1:1; :: thesis: verum

end;

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