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 A3: B c= Rank B ; :: thesis: S₁[ succ B]
A4: B in Rank (succ B) by A3, Th36;
A5: ( B c= Rank (succ B) & {B} c= Rank (succ B) ) by A4, ORDINAL1:def 2, ZFMISC_1:37;
thus S₁[ succ B] by A5, XBOOLE_1:8; :: thesis: verum

end;

A6: 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
A <> {} and
A7: A is limit_ordinal and
A8: 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 A9: x in A ; :: thesis: x in Rank A
reconsider B = x as Ordinal by A9;
A10: succ B in A by A7, A9, ORDINAL1:41;
A11: B c= Rank B by A8, A9;
A12: succ B c= A by A10, ORDINAL1:def 2;
A13: B in Rank (succ B) by A11, Th36;
A14: Rank (succ B) c= Rank A by A12, Th43;
thus x in Rank A by A13, A14; :: thesis: verum

end;

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