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 S1[ Ordinal] means $1 c= the_rank_of $1;
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2: for B being Ordinal st B in A holds
B c= the_rank_of B ; :: thesis: S1[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 S1[A] by Th70; :: thesis: verum
end;
for B being Ordinal holds S1[B] from ORDINAL1:sch 2(A1);
 hence A c= the_rank_of A ; :: thesis: verum