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 and
A8: X in Rank B by A3, Lm2, Th35;
X c= Rank B by A2, A7, A8;
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
A9: A = succ B by ORDINAL1:29;
X c= Rank B by A3, A9, Th36;
then x c= Rank B by A2, A4, A9, ORDINAL1:6;
hence x in Rank A by A9, 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