let A be Ordinal; :: thesis: for x being Surreal st x in Day A holds
x <= No_Ordinal_op A
let x be Surreal; :: thesis: ( x in Day A implies x <= No_Ordinal_op A )
defpred S₁[ Ordinal] means for x being Surreal st x in Day $1 holds
x <= No_Ordinal_op $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]
set O = No_Ordinal_op D;
let x be Surreal; :: thesis: ( x in Day D implies x <= No_Ordinal_op D )
assume A3: x in Day D ; :: thesis: x <= No_Ordinal_op D
L_ x << {(No_Ordinal_op D)}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ x or not b in {(No_Ordinal_op D)} or not b <= a )
assume A4: ( a in L_ x & b in {(No_Ordinal_op D)} ) ; :: thesis: not b <= a
A5: a in (L_ x) \/ (R_ x) by XBOOLE_0:def 3, A4;
then A6: born a in born x by SURREALO:1;
A7: No_Ordinal_op (born a) < No_Ordinal_op (born x) by A5, SURREALO:1, Th68;
A8: born x c= D by A3, SURREAL0:def 18;
then A9: No_Ordinal_op (born x) <= No_Ordinal_op D by Th68, ORDINAL1:5;
a in Day (born a) by SURREAL0:def 18;
then a <= No_Ordinal_op (born a) by A2, A6, A8;
then a < No_Ordinal_op (born x) by A7, SURREALO:4;
then a < No_Ordinal_op D by A9, SURREALO:4;
hence not b <= a by A4, TARSKI:def 1; :: thesis: verum

end;

then ( L_ x << {(No_Ordinal_op D)} & {x} << R_ (No_Ordinal_op D) ) by Def10;
hence x <= No_Ordinal_op D by SURREAL0:43; :: thesis: verum

end;

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