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
consider B being Ordinal such that
A7: B in A and
A8: X in Rank B by A3, A6, Lm2, Th35;
A9: X c= Rank B by A2, A7, A8;
thus x in Rank A by A4, A6, A7, A9, Th35; :: thesis: verum

end;

A10: now

assume A11: not A is limit_ordinal ; :: thesis: x in Rank A
consider B being Ordinal such that
A12: A = succ B by A11, ORDINAL1:42;
A13: X c= Rank B by A3, A12, Th36;
A14: x c= Rank B by A2, A4, A12, A13, ORDINAL1:10;
thus x in Rank A by A12, A14, Th36; :: thesis: verum

end;

thus x in Rank A by A5, A10; :: thesis: verum

end;

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