let A be Ordinal; :: thesis: A c= Rank A
defpred S₁[ Ordinal] means $1 c= Rank $1;
A1: S₁[ {} ] by XBOOLE_1:2;
A2: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume B c= Rank B ; :: thesis: S₁[ succ B]
then B in Rank (succ B) by Th36;
then ( B c= Rank (succ B) & {B} c= Rank (succ B) ) by ORDINAL1:def 2, ZFMISC_1:37;
hence S₁[ succ B] by XBOOLE_1:8; :: thesis: verum

end;

A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A4: ( A <> {} & A is limit_ordinal ) and
A5: for B being Ordinal st B in A holds
B c= Rank B ; :: thesis: S₁[A]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Rank A )
assume A6: x in A ; :: thesis: x in Rank A
then reconsider B = x as Ordinal ;
succ B in A by A4, A6, ORDINAL1:41;
then ( B c= Rank B & succ B c= A ) by A5, A6, ORDINAL1:def 2;
then ( B in Rank (succ B) & Rank (succ B) c= Rank A ) by Th36, Th43;
hence x in Rank A ; :: thesis: verum

end;

for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A1, A2, A3);
hence A c= Rank A ; :: thesis: verum