let A be Ordinal; :: thesis: the_rank_of A = A
A c= Rank A by Th38;
hence the_rank_of A c= A by Th65; :: according to XBOOLE_0:def 10 :: thesis: A c= the_rank_of A
defpred S₁[ Ordinal] means $1 c= the_rank_of $1;
A1: 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 A2: for B being Ordinal st B in A holds
B c= the_rank_of B ; :: thesis: S₁[A]

now :: thesis: for B being Ordinal st B in A holds
ex Y being set st
( Y in A & B c= the_rank_of Y )

let B be Ordinal; :: thesis: ( B in A implies ex Y being set st
( Y in A & B c= the_rank_of Y ) )
assume A3: 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 A2, A3; :: thesis: verum

end;

hence S₁[A] by Th70; :: thesis: verum

end;

for B being Ordinal holds S₁[B] from ORDINAL1:sch 2(A1);
hence A c= the_rank_of A ; :: thesis: verum