let A be Ordinal; :: thesis: the_rank_of A = A
A1: A c= Rank A by Th44;
thus the_rank_of A c= A by A1, Th73; :: according to XBOOLE_0:def 10 :: thesis: A c= the_rank_of A
defpred S₁[ Ordinal] means $1 c= the_rank_of $1;
A2: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume A3: for B being Ordinal st B in A holds
B c= the_rank_of B ; :: thesis: S₁[A]

A4: now

let B be Ordinal; :: thesis: ( B in A implies ex Y being set st
( Y in A & B c= the_rank_of Y ) )
assume A5: B in A ; :: thesis: ex Y being set st
( Y in A & B c= the_rank_of Y )
reconsider Y = B as set ;
take Y = Y; :: thesis: ( Y in A & B c= the_rank_of Y )
thus ( Y in A & B c= the_rank_of Y ) by A3, A5; :: thesis: verum

end;

thus S₁[A] by A4, Th78; :: thesis: verum

end;

A6: for B being Ordinal holds S₁[B] from ORDINAL1:sch 2(A2);
thus A c= the_rank_of A by A6; :: thesis: verum