defpred S₁[ Ordinal] means ex A1, A2 being Ordinal st
( A1 is limit_ordinal & A2 is natural & $1 = A1 +^ A2 );
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]
A3: ( ex B being Ordinal st A = succ B implies S₁[A] )

proof

given B being Ordinal such that A4: A = succ B ; :: thesis: S₁[A]
consider C, D being Ordinal such that
A5: C is limit_ordinal and
A6: D is natural and
A7: B = C +^ D by A2, A4, ORDINAL1:6;
take C ; :: thesis: ex A2 being Ordinal st
( C is limit_ordinal & A2 is natural & A = C +^ A2 )
take E = succ D; :: thesis: ( C is limit_ordinal & E is natural & A = C +^ E )
thus C is limit_ordinal by A5; :: thesis: ( E is natural & A = C +^ E )
thus E in omega by A6, ORDINAL1:def 12; :: according to ORDINAL1:def 12 :: thesis: A = C +^ E
thus A = C +^ E by A4, A7, Th28; :: thesis: verum

end;

( ( for B being Ordinal holds A <> succ B ) implies S₁[A] )

proof

assume A8: for D being Ordinal holds A <> succ D ; :: thesis: S₁[A]
take B = A; :: thesis: ex A2 being Ordinal st
( B is limit_ordinal & A2 is natural & A = B +^ A2 )
take C = 0 ; :: thesis: ( B is limit_ordinal & C is natural & A = B +^ C )
thus B is limit_ordinal by A8, ORDINAL1:29; :: thesis: ( C is natural & A = B +^ C )
thus C in omega by ORDINAL1:def 11; :: according to ORDINAL1:def 12 :: thesis: A = B +^ C
thus A = B +^ C by Th27; :: thesis: verum

end;

hence S₁[A] by A3; :: thesis: verum

end;

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