let x, Min be Surreal; :: thesis:
assume that
A1: for y being Surreal st y in R_ x holds
Min <= y and
A2: Min in R_ x ; :: thesis:
A3: L_ x << R_ x by SURREAL0:45;
A4: L_ x << {Min}

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A5: ( l in L_ x & r in {Min} ) ; :: thesis:
r = Min by A5, TARSKI:def 1;
hence not l >= r by A3, A5, A2; :: thesis:

end;

for o being object st o in (L_ x) \/ {Min} holds
ex O being Ordinal st
( O in born x & o in Day O )

let o be object ; :: thesis:
assume A6: o in (L_ x) \/ {Min} ; :: thesis:
( o = Min or o in L_ x ) by A6, ZFMISC_1:136;
then A7: o in (L_ x) \/ (R_ x) by A2, XBOOLE_0:def 3;
reconsider o = o as Surreal by SURREAL0:def 16, A6;
take born o ; :: thesis:
thus ( born o in born x & o in Day (born o) ) by A7, Th1, SURREAL0:def 18; :: thesis:

end;

then A8: [(L_ x),{Min}] in Day (born x) by A4, SURREAL0:46;
hence [(L_ x),{Min}] is Surreal ; :: thesis:
let y be Surreal; :: thesis:
assume A9: y = [(L_ x),{Min}] ; :: thesis:
A10: ( x = [(L_ x),(R_ x)] & y = [(L_ y),(R_ y)] ) ;
A11: for x1 being Surreal st x1 in L_ x holds
ex y1 being Surreal st
( y1 in L_ y & x1 <= y1 ) by A9;
A12: for x1 being Surreal st x1 in R_ y holds
ex y1 being Surreal st
( y1 in R_ x & y1 <= x1 )

let x1 be Surreal; :: thesis:
assume A13: x1 in R_ y ; :: thesis:
take Min ; :: thesis:
thus ( Min in R_ x & Min <= x1 ) by A9, A13, A2, TARSKI:def 1; :: thesis:

end;

A14: for x1 being Surreal st x1 in L_ y holds
ex y1 being Surreal st
( y1 in L_ x & x1 <= y1 ) by A9;
for x1 being Surreal st x1 in R_ x holds
ex y1 being Surreal st
( y1 in R_ y & y1 <= x1 )

let x1 be Surreal; :: thesis:
assume A15: x1 in R_ x ; :: thesis:
take Min ; :: thesis:
thus ( Min in R_ y & Min <= x1 ) by A15, A1, A9, TARSKI:def 1; :: thesis:

end;

hence ( y == x & born y c= born x ) by A10, A14, SURREAL0:44, A12, A11, SURREAL0:def 18, A9, A8; :: thesis: