let A be Ordinal; :: thesis: No_Ordinal_op A in Day A
defpred S₁[ Ordinal] means No_Ordinal_op $1 in Day $1;
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]

per cases ( D is limit_ordinal or not D is limit_ordinal ) ;

suppose D is limit_ordinal ; :: thesis: S₁[D]

then consider X being set such that
A3: ( No_Ordinal_op D = [X,{}] & ( for o being object holds
( o in X iff ex B being Ordinal st
( B in D & o = No_Ordinal_op B ) ) ) ) by Th66;
A4: X << {} ;
for o being object st o in X \/ {} holds
ex O being Ordinal st
( O in D & o in Day O )

proof

let o be object ; :: thesis: ( o in X \/ {} implies ex O being Ordinal st
( O in D & o in Day O ) )
assume o in X \/ {} ; :: thesis: ex O being Ordinal st
( O in D & o in Day O )
then consider B being Ordinal such that
A5: ( B in D & o = No_Ordinal_op B ) by A3;
No_Ordinal_op B in Day B by A5, A2;
hence ex O being Ordinal st
( O in D & o in Day O ) by A5; :: thesis: verum

end;

hence S₁[D] by A3, A4, SURREAL0:46; :: thesis: verum

end;

suppose not D is limit_ordinal ; :: thesis: S₁[D]

then consider B being Ordinal such that
A6: succ B = D by ORDINAL1:29;
A7: No_Ordinal_op B in Day B by A6, ORDINAL1:6, A2;
then reconsider OB = No_Ordinal_op B as Surreal ;
A8: {OB} << {} ;
for o being object st o in {OB} \/ {} holds
ex O being Ordinal st
( O in D & o in Day O )

proof

let o be object ; :: thesis: ( o in {OB} \/ {} implies ex O being Ordinal st
( O in D & o in Day O ) )
assume o in {OB} \/ {} ; :: thesis: ex O being Ordinal st
( O in D & o in Day O )
then o = OB by TARSKI:def 1;
hence ex O being Ordinal st
( O in D & o in Day O ) by A7, A6, ORDINAL1:6; :: thesis: verum

end;

then [{OB},{}] in Day D by A8, SURREAL0:46;
hence S₁[D] by A6, Th65; :: thesis: verum

end;

end;

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence No_Ordinal_op A in Day A ; :: thesis: verum