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]

let A be Ordinal; :: thesis:
assume A2: for B being Ordinal st B in A holds
S₁[B] ; :: thesis:
A3: ( ex B being Ordinal st A = succ B implies S₁[A] )

given B being Ordinal such that A4: A = succ B ; :: thesis:
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:
take E = succ D; :: thesis:
thus C is limit_ordinal by A5; :: thesis:
thus E in omega by A6, ORDINAL1:def 12; :: according to ORDINAL1:def 12 :: thesis:
thus A = C +^ E by A4, A7, Th28; :: thesis:

end;

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

assume A8: for D being Ordinal holds A <> succ D ; :: thesis:
take B = A; :: thesis:
take C = 0 ; :: thesis:
thus B is limit_ordinal by A8, ORDINAL1:29; :: thesis:
thus C in omega by ORDINAL1:def 11; :: according to ORDINAL1:def 12 :: thesis:
thus A = B +^ C by Th27; :: thesis:

end;

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

end;

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