let x, Max be Surreal; :: thesis: ( ( for y being Surreal st y in L_ x holds
y <= Max ) & Max in L_ x implies ( [{Max},(R_ x)] is Surreal & ( for y being Surreal st y = [{Max},(R_ x)] holds
( y == x & born y c= born x ) ) ) )
assume that
A1: for y being Surreal st y in L_ x holds
y <= Max and
A2: Max in L_ x ; :: thesis: ( [{Max},(R_ x)] is Surreal & ( for y being Surreal st y = [{Max},(R_ x)] holds
( y == x & born y c= born x ) ) )
A3: L_ x << R_ x by SURREAL0:45;
A4: {Max} << R_ x

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in {Max} or not b₁ in R_ x or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in {Max} or not r in R_ x or not l >= r )
assume A5: ( l in {Max} & r in R_ x ) ; :: thesis: not l >= r
l = Max by A5, TARSKI:def 1;
hence not l >= r by A3, A5, A2; :: thesis: verum

end;

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

proof

let o be object ; :: thesis: ( o in {Max} \/ (R_ x) implies ex O being Ordinal st
( O in born x & o in Day O ) )
assume A6: o in {Max} \/ (R_ x) ; :: thesis: ex O being Ordinal st
( O in born x & o in Day O )
( o = Max or o in R_ 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: ( born o in born x & o in Day (born o) )
thus ( born o in born x & o in Day (born o) ) by SURREAL0:def 18, A7, Th1; :: thesis: verum

end;

then A8: [{Max},(R_ x)] in Day (born x) by A4, SURREAL0:46;
hence [{Max},(R_ x)] is Surreal ; :: thesis: for y being Surreal st y = [{Max},(R_ x)] holds
( y == x & born y c= born x )
let y be Surreal; :: thesis: ( y = [{Max},(R_ x)] implies ( y == x & born y c= born x ) )
assume A9: y = [{Max},(R_ x)] ; :: thesis: ( y == x & born y c= born x )
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 )

proof

let x1 be Surreal; :: thesis: ( x1 in L_ x implies ex y1 being Surreal st
( y1 in L_ y & x1 <= y1 ) )
assume A12: x1 in L_ x ; :: thesis: ex y1 being Surreal st
( y1 in L_ y & x1 <= y1 )
take Max ; :: thesis: ( Max in L_ y & x1 <= Max )
thus ( Max in L_ y & x1 <= Max ) by A12, A1, A9, TARSKI:def 1; :: thesis: verum

end;

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

proof

let x1 be Surreal; :: thesis: ( x1 in L_ y implies ex y1 being Surreal st
( y1 in L_ x & x1 <= y1 ) )
assume A15: x1 in L_ y ; :: thesis: ex y1 being Surreal st
( y1 in L_ x & x1 <= y1 )
take Max ; :: thesis: ( Max in L_ x & x1 <= Max )
thus ( Max in L_ x & x1 <= Max ) by A15, A2, A9, TARSKI:def 1; :: thesis: verum

end;

for x1 being Surreal st x1 in R_ x holds
ex y1 being Surreal st
( y1 in R_ y & y1 <= x1 ) by A9;
hence ( y == x & born y c= born x ) by SURREAL0:def 18, A9, A8, A13, A10, A14, SURREAL0:44, A11; :: thesis: verum