defpred S₁[ Ordinal] means ( ( for x being Surreal st x in Day $1 holds
( - x is surreal & - x in Day $1 & ( for x1 being Surreal st x1 = - x holds
- x1 = x ) ) ) & ( for x, x1, y, y1 being Surreal st x in Day $1 & y in Day $1 & x1 = - x & y1 = - y holds
( x <= y iff y1 <= x1 ) ) );
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]
thus A3: for x being Surreal st x in Day D holds
( - x is surreal & - x in Day D & ( for x1 being Surreal st x1 = - x holds
- x1 = x ) ) :: thesis: for x, x1, y, y1 being Surreal st x in Day D & y in Day D & x1 = - x & y1 = - y holds
( x <= y iff y1 <= x1 )

proof

let x be Surreal; :: thesis: ( x in Day D implies ( - x is surreal & - x in Day D & ( for x1 being Surreal st x1 = - x holds
- x1 = x ) ) )
assume A4: x in Day D ; :: thesis: ( - x is surreal & - x in Day D & ( for x1 being Surreal st x1 = - x holds
- x1 = x ) )
A5: x = [(L_ x),(R_ x)] ;
then A6: L_ x << R_ x by A4, SURREAL0:46;
A7: -- (R_ x) << -- (L_ x)

proof

let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in -- (R_ x) or not r in -- (L_ x) or not r <= l )
assume A8: ( l in -- (R_ x) & r in -- (L_ x) ) ; :: thesis: not r <= l
consider L being Surreal such that
A9: ( L in R_ x & l = - L ) by A8, Def4;
consider R being Surreal such that
A10: ( R in L_ x & r = - R ) by A8, Def4;
L in (L_ x) \/ (R_ x) by A9, XBOOLE_0:def 3;
then consider OL being Ordinal such that
A11: ( OL in D & L in Day OL ) by A4, A5, SURREAL0:46;
A12: not L <= R by A6, A10, A9;
R in (L_ x) \/ (R_ x) by A10, XBOOLE_0:def 3;
then consider OR being Ordinal such that
A13: ( OR in D & R in Day OR ) by A4, A5, SURREAL0:46;
set O = OL \/ OR;
A14: ( Day OL c= Day (OL \/ OR) & Day OR c= Day (OL \/ OR) ) by SURREAL0:35, XBOOLE_1:7;
OL \/ OR in D by ORDINAL3:12, A11, A13;
hence not r <= l by A2, A12, A14, A9, A10, A13, A11; :: thesis: verum

end;

for y being object st y in (-- (R_ x)) \/ (-- (L_ x)) holds
ex O being Ordinal st
( O in D & y in Day O )

proof

let y be object ; :: thesis: ( y in (-- (R_ x)) \/ (-- (L_ x)) implies ex O being Ordinal st
( O in D & y in Day O ) )
assume A15: y in (-- (R_ x)) \/ (-- (L_ x)) ; :: thesis: ex O being Ordinal st
( O in D & y in Day O )

per cases ( y in -- (R_ x) or y in -- (L_ x) ) by A15, XBOOLE_0:def 3;

suppose y in -- (R_ x) ; :: thesis: ex O being Ordinal st
( O in D & y in Day O )

then consider L being Surreal such that
A16: ( L in R_ x & y = - L ) by Def4;
L in (L_ x) \/ (R_ x) by A16, XBOOLE_0:def 3;
then consider OL being Ordinal such that
A17: ( OL in D & L in Day OL ) by A4, A5, SURREAL0:46;
S₁[OL] by A17, A2;
hence ex O being Ordinal st
( O in D & y in Day O ) by A16, A17; :: thesis: verum

end;

suppose y in -- (L_ x) ; :: thesis: ex O being Ordinal st
( O in D & y in Day O )

then consider L being Surreal such that
A18: ( L in L_ x & y = - L ) by Def4;
L in (L_ x) \/ (R_ x) by A18, XBOOLE_0:def 3;
then consider OL being Ordinal such that
A19: ( OL in D & L in Day OL ) by A4, A5, SURREAL0:46;
S₁[OL] by A19, A2;
hence ex O being Ordinal st
( O in D & y in Day O ) by A18, A19; :: thesis: verum

end;

end;

end;

then [(-- (R_ x)),(-- (L_ x))] in Day D by A7, SURREAL0:46;
hence ( - x is surreal & - x in Day D ) by Th7; :: thesis: for x1 being Surreal st x1 = - x holds
- x1 = x
let x1 be Surreal; :: thesis: ( x1 = - x implies - x1 = x )
assume A20: x1 = - x ; :: thesis: - x1 = x
A21: x1 = [(-- (R_ x)),(-- (L_ x))] by A20, Th7;
A22: - x1 = [(-- (R_ x1)),(-- (L_ x1))] by Th7;
A23: -- (R_ x1) c= L_ x

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in -- (R_ x1) or y in L_ x )
assume y in -- (R_ x1) ; :: thesis: y in L_ x
then consider y1 being Surreal such that
A24: ( y1 in R_ x1 & - y1 = y ) by Def4;
consider y2 being Surreal such that
A25: ( y2 in L_ x & - y2 = y1 ) by A21, A24, Def4;
y2 in (L_ x) \/ (R_ x) by A25, XBOOLE_0:def 3;
then A26: ( born y2 in born x & born x c= D ) by A4, SURREALO:1, SURREAL0:def 18;
y2 in Day (born y2) by SURREAL0:def 18;
hence y in L_ x by A25, A2, A26, A24; :: thesis: verum

end;

L_ x c= -- (R_ x1)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in L_ x or y in -- (R_ x1) )
assume A27: y in L_ x ; :: thesis: y in -- (R_ x1)
then reconsider y = y as Surreal by SURREAL0:def 16;
y in (L_ x) \/ (R_ x) by A27, XBOOLE_0:def 3;
then A28: ( born y in born x & born x c= D & y in Day (born y) ) by A4, SURREALO:1, SURREAL0:def 18;
then reconsider y1 = - y as Surreal by A2;
y1 in R_ x1 by A21, A27, Def4;
then - y1 in -- (R_ x1) by Def4;
hence y in -- (R_ x1) by A28, A2; :: thesis: verum

end;

then A29: L_ x = -- (R_ x1) by A23, XBOOLE_0:def 10;
A30: -- (L_ x1) c= R_ x

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in -- (L_ x1) or y in R_ x )
assume y in -- (L_ x1) ; :: thesis: y in R_ x
then consider y1 being Surreal such that
A31: ( y1 in L_ x1 & - y1 = y ) by Def4;
consider y2 being Surreal such that
A32: ( y2 in R_ x & - y2 = y1 ) by A21, A31, Def4;
y2 in (L_ x) \/ (R_ x) by A32, XBOOLE_0:def 3;
then A33: ( born y2 in born x & born x c= D ) by A4, SURREALO:1, SURREAL0:def 18;
y2 in Day (born y2) by SURREAL0:def 18;
hence y in R_ x by A32, A2, A33, A31; :: thesis: verum

end;

R_ x c= -- (L_ x1)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R_ x or y in -- (L_ x1) )
assume A34: y in R_ x ; :: thesis: y in -- (L_ x1)
then reconsider y = y as Surreal by SURREAL0:def 16;
y in (L_ x) \/ (R_ x) by A34, XBOOLE_0:def 3;
then A35: ( born y in born x & born x c= D & y in Day (born y) ) by A4, SURREALO:1, SURREAL0:def 18;
then reconsider y1 = - y as Surreal by A2;
y1 in L_ x1 by A21, A34, Def4;
then - y1 in -- (L_ x1) by Def4;
hence y in -- (L_ x1) by A35, A2; :: thesis: verum

end;

then R_ x = -- (L_ x1) by A30, XBOOLE_0:def 10;
hence - x1 = x by A22, A29; :: thesis: verum

end;

defpred S₂[ Ordinal] means for x, x1, y, y1 being Surreal st x in Day D & y in Day D & x1 = - x & y1 = - y & (born x) (+) (born y) c= $1 holds
( x <= y iff y1 <= x1 );
A36: for E being Ordinal st ( for F being Ordinal st F in E holds
S₂[F] ) holds
S₂[E]

proof

let E be Ordinal; :: thesis: ( ( for F being Ordinal st F in E holds
S₂[F] ) implies S₂[E] )
assume A37: for C being Ordinal st C in E holds
S₂[C] ; :: thesis: S₂[E]
A38: for x, x1, y, y1 being Surreal st x in Day D & y in Day D & x1 = - x & y1 = - y & (born x) (+) (born y) c= E & x <= y holds
y1 <= x1

proof

let x, x1, y, y1 be Surreal; :: thesis: ( x in Day D & y in Day D & x1 = - x & y1 = - y & (born x) (+) (born y) c= E & x <= y implies y1 <= x1 )
assume A39: ( x in Day D & y in Day D & x1 = - x & y1 = - y & (born x) (+) (born y) c= E & x <= y ) ; :: thesis: y1 <= x1
A40: ( - x = [(-- (R_ x)),(-- (L_ x))] & - y = [(-- (R_ y)),(-- (L_ y))] ) by Th7;
A41: ( x in Day (born x) & born x c= D ) by A39, SURREAL0:def 18;
A42: ( y in Day (born y) & born y c= D ) by A39, SURREAL0:def 18;
A43: ( L_ x << {y} & {x} << R_ y ) by A39, SURREAL0:43;
A44: {y1} << R_ x1

proof

let r, l1 be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not r in {y1} or not l1 in R_ x1 or not l1 <= r )
assume A45: ( r in {y1} & l1 in R_ x1 ) ; :: thesis: not l1 <= r
consider l being Surreal such that
A46: ( l in L_ x & l1 = - l ) by A45, A39, A40, Def4;
A47: l in (L_ x) \/ (R_ x) by XBOOLE_0:def 3, A46;
then A48: born l in born x by SURREALO:1;
A49: (born l) (+) (born y) in (born x) (+) (born y) by A47, SURREALO:1, ORDINAL7:94;
A50: ( l in Day (born l) & Day (born l) c= Day D ) by A41, A48, SURREAL0:def 18, SURREAL0:35, ORDINAL1:def 2;
A51: r = y1 by A45, TARSKI:def 1;
y in {y} by TARSKI:def 1;
then not y <= l by A43, A46;
hence not l1 <= r by A50, A49, A39, A37, A46, A51; :: thesis: verum

end;

L_ y1 << {x1}

proof

let l1, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l1 in L_ y1 or not r in {x1} or not r <= l1 )
assume A52: ( l1 in L_ y1 & r in {x1} ) ; :: thesis: not r <= l1
consider l being Surreal such that
A53: ( l in R_ y & l1 = - l ) by A52, A39, A40, Def4;
A54: l in (L_ y) \/ (R_ y) by XBOOLE_0:def 3, A53;
then A55: born l in born y by SURREALO:1;
A56: (born l) (+) (born x) in (born x) (+) (born y) by A54, SURREALO:1, ORDINAL7:94;
A57: ( l in Day (born l) & Day (born l) c= Day D ) by A42, A55, SURREAL0:def 18, SURREAL0:35, ORDINAL1:def 2;
A58: r = x1 by A52, TARSKI:def 1;
x in {x} by TARSKI:def 1;
then not l <= x by A43, A53;
hence not r <= l1 by A58, A57, A56, A39, A37, A53; :: thesis: verum

end;

hence y1 <= x1 by A44, SURREAL0:43; :: thesis: verum

end;

let x, x1, y, y1 be Surreal; :: thesis: ( x in Day D & y in Day D & x1 = - x & y1 = - y & (born x) (+) (born y) c= E implies ( x <= y iff y1 <= x1 ) )
assume A59: ( x in Day D & y in Day D & x1 = - x & y1 = - y & (born x) (+) (born y) c= E ) ; :: thesis: ( x <= y iff y1 <= x1 )
thus ( x <= y implies y1 <= x1 ) by A59, A38; :: thesis: ( y1 <= x1 implies x <= y )
A60: x in Day (born x) by SURREAL0:def 18;
born x c= D by A59, SURREAL0:def 18;
then ( born x = D or born x in D ) by ORDINAL1:11, XBOOLE_0:def 8;
then x1 in Day (born x) by A60, A3, A2, A59;
then A61: born x1 c= born x by SURREAL0:def 18;
A62: x1 in Day (born x1) by SURREAL0:def 18;
A63: x1 in Day D by A3, A59;
then born x1 c= D by SURREAL0:def 18;
then A64: ( born x1 = D or born x1 in D ) by ORDINAL1:11, XBOOLE_0:def 8;
A65: - x1 = x by A3, A59;
then x in Day (born x1) by A62, A64, A3, A2;
then born x c= born x1 by SURREAL0:def 18;
then A66: born x = born x1 by A61, XBOOLE_0:def 10;
A67: y in Day (born y) by SURREAL0:def 18;
born y c= D by A59, SURREAL0:def 18;
then ( born y = D or born y in D ) by ORDINAL1:11, XBOOLE_0:def 8;
then y1 in Day (born y) by A67, A3, A2, A59;
then A68: born y1 c= born y by SURREAL0:def 18;
A69: y1 in Day (born y1) by SURREAL0:def 18;
A70: y1 in Day D by A3, A59;
then born y1 c= D by SURREAL0:def 18;
then A71: ( born y1 = D or born y1 in D ) by ORDINAL1:11, XBOOLE_0:def 8;
A72: - y1 = y by A3, A59;
then y in Day (born y1) by A69, A71, A3, A2;
then born y c= born y1 by SURREAL0:def 18;
then born y = born y1 by A68, XBOOLE_0:def 10;
hence ( y1 <= x1 implies x <= y ) by A59, A38, A66, A65, A72, A70, A63; :: thesis: verum

end;

A73: for E being Ordinal holds S₂[E] from ORDINAL1:sch 2(A36);
let x, x1, y, y1 be Surreal; :: thesis: ( x in Day D & y in Day D & x1 = - x & y1 = - y implies ( x <= y iff y1 <= x1 ) )
assume A74: ( x in Day D & y in Day D & x1 = - x & y1 = - y ) ; :: thesis: ( x <= y iff y1 <= x1 )
S₂[(born x) (+) (born y)] by A73;
hence ( x <= y iff y1 <= x1 ) by A74; :: thesis: verum

end;

for E being Ordinal holds S₁[E] from ORDINAL1:sch 2(A1);
hence for D being Ordinal holds
( ( for x being Surreal st x in Day D holds
( - x is surreal & - x in Day D & ( for x1 being Surreal st x1 = - x holds
- x1 = x ) ) ) & ( for x, x1, y, y1 being Surreal st x in Day D & y in Day D & x1 = - x & y1 = - y holds
( x <= y iff y1 <= x1 ) ) ) ; :: thesis: verum