let A be Ordinal; :: thesis: A c= Rank A
defpred S₁[ Ordinal] means $1 c= Rank $1;
A1: S₁[ 0 ] 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 Th32;
then ( B c= Rank (succ B) & {B} c= Rank (succ B) ) by ORDINAL1:def 2, ZFMISC_1:31;
hence S₁[ succ B] by XBOOLE_1:8; :: thesis: verum

end;

A3: for A being Ordinal st A <> 0 & 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 <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume that
A <> 0 and
A4: 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 object ; :: 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 ;
A7: B c= Rank B by A5, A6;
A8: succ B c= A by A4, A6, ORDINAL1:28, ORDINAL1:def 2;
A9: B in Rank (succ B) by A7, Th32;
Rank (succ B) c= Rank A by A8, Th37;
hence x in Rank A by A9; :: thesis: verum

end;

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