defpred S₁[ Ordinal] means for X being set st X in Rank A holds
X c= Rank A;
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
S₁[B] ; :: thesis: S₁[A]
let X be set ; :: thesis: ( X in Rank A implies X c= Rank A )
assume A3: X in Rank A ; :: thesis: X c= Rank A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Rank A )
assume A4: x in X ; :: thesis: x in Rank A

A5: now

assume A6: A is limit_ordinal ; :: thesis: x in Rank A
then consider B being Ordinal such that
A7: ( B in A & X in Rank B ) by A3, Lm2, Th35;
X c= Rank B by A2, A7;
hence x in Rank A by A4, A6, A7, Th35; :: thesis: verum

end;

now

assume not A is limit_ordinal ; :: thesis: x in Rank A
then consider B being Ordinal such that
A8: A = succ B by ORDINAL1:42;
( B in A & X c= Rank B ) by A3, A8, Th36, ORDINAL1:10;
then x c= Rank B by A2, A4;
hence x in Rank A by A8, Th36; :: thesis: verum

end;

hence x in Rank A by A5; :: thesis: verum

end;

for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A1);
hence S₁[A] ; :: according to ORDINAL1:def 2 :: thesis: verum