let x, y be Surreal; :: thesis: ( L_ y << {x} & {x} << R_ y & ( for z being Surreal st L_ y << {z} & {z} << R_ y holds
born x c= born z ) implies x == y )
assume that
A1: ( L_ y << {x} & {x} << R_ y ) and
A2: for x1 being Surreal st L_ y << {x1} & {x1} << R_ y holds
born x c= born x1 ; :: thesis: x == y
set X = (L_ x) \/ (L_ y);
set Y = (R_ x) \/ (R_ y);
A3: x in {x} by TARSKI:def 1;
reconsider z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] as Surreal by Th14, A1;
A4: ( L_ x << {x} & {x} << R_ x ) by Th11;
A5: ( L_ y << {y} & {y} << R_ y ) by Th11;
A6: ( L_ z << {z} & {z} << R_ z ) by Th11;
A7: L_ x << {z}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ x or not b in {z} or not a >= b )
assume A8: ( a in L_ x & b in {z} ) ; :: thesis: not a >= b
then a in L_ z by XBOOLE_0:def 3;
hence a < b by A8, A6; :: thesis: verum

end;

{x} << R_ z

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in {x} or not b in R_ z or not a >= b )
assume A9: ( a in {x} & b in R_ z ) ; :: thesis: not a >= b
then ( b in R_ x or b in R_ y ) by XBOOLE_0:def 3;
hence a < b by A4, A9, A1; :: thesis: verum

end;

then A10: x <= z by A7, SURREAL0:43;
A11: L_ y << {z}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in L_ y or not b in {z} or not a >= b )
assume A12: ( a in L_ y & b in {z} ) ; :: thesis: not a >= b
then a < z by A1, A3, A10, Th4;
hence not a >= b by A12, TARSKI:def 1; :: thesis: verum

end;

A13: x == z by Th15, A1;
A14: {y} << R_ z

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in {y} or not b in R_ z or not a >= b )
assume A15: ( a in {y} & b in R_ z ) ; :: thesis: not a >= b

per cases then ( b in R_ y or b in R_ x ) by XBOOLE_0:def 3;

suppose b in R_ y ; :: thesis: not a >= b

hence not a >= b by A5, A15; :: thesis: verum

end;

suppose A16: b in R_ x ; :: thesis: not a >= b

assume not a < b ; :: thesis: contradiction
then b <= y by A15, TARSKI:def 1;
then A17: {b} << R_ y by SURREAL0:43;
L_ y << {b}

proof

let c, d be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not c in L_ y or not d in {b} or not c >= d )
assume A18: ( c in L_ y & d in {b} ) ; :: thesis: not c >= d
then c <= x by A3, A1;
then c < b by A4, A3, A16, Th4;
hence c < d by A18, TARSKI:def 1; :: thesis: verum

end;

then A19: born x c= born b by A17, A2;
A20: b in (L_ x) \/ (R_ x) by A16, XBOOLE_0:def 3;
then A21: born b in born x by Th1;
born b c= born x by A20, Th1, ORDINAL1:def 2;
then born b = born x by A19, XBOOLE_0:def 10;
hence contradiction by A21; :: thesis: verum

end;

end;

end;

A22: {z} << R_ y

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not a in {z} or not b in R_ y or not a >= b )
assume A23: ( a in {z} & b in R_ y ) ; :: thesis: not a >= b
then z < b by A1, A3, A13, Th4;
hence not a >= b by A23, TARSKI:def 1; :: thesis: verum

end;

L_ z << {y}

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not b in L_ z or not a in {y} or not b >= a )
assume A24: ( b in L_ z & a in {y} ) ; :: thesis: not b >= a

per cases then ( b in L_ y or b in L_ x ) by XBOOLE_0:def 3;

suppose b in L_ y ; :: thesis: not b >= a

hence not b >= a by A5, A24; :: thesis: verum

end;

suppose A25: b in L_ x ; :: thesis: not b >= a

assume not b < a ; :: thesis: contradiction
then y <= b by A24, TARSKI:def 1;
then A26: L_ y << {b} by SURREAL0:43;
{b} << R_ y

proof

let d, c be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not d in {b} or not c in R_ y or not d >= c )
assume A27: ( d in {b} & c in R_ y ) ; :: thesis: not d >= c
then x <= c by A3, A1;
then b < c by A4, A3, A25, Th4;
hence d < c by A27, TARSKI:def 1; :: thesis: verum

end;

then A28: born x c= born b by A26, A2;
A29: b in (L_ x) \/ (R_ x) by A25, XBOOLE_0:def 3;
then A30: born b in born x by Th1;
born b c= born x by A29, Th1, ORDINAL1:def 2;
then born b = born x by A28, XBOOLE_0:def 10;
hence contradiction by A30; :: thesis: verum

end;

end;

end;

then z == y by A22, SURREAL0:43, A14, A11;
hence x == y by A13, Th4; :: thesis: verum