let x, y, z be Surreal; :: thesis: ( L_ y << {x} & {x} << R_ y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] implies x == z )
assume that
A1: ( L_ y << {x} & {x} << R_ y ) and
A2: z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] ; :: thesis: x == z
A3: ( L_ x << {x} & {x} << R_ x ) by Th11;
A4: ( L_ z << {z} & {z} << R_ z ) by Th11;
A5: L_ z << {x}

proof

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

end;

A7: {z} << R_ x

proof

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

end;

A9: 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 A10: ( a in L_ x & b in {z} ) ; :: thesis: not a >= b
then a in L_ z by A2, XBOOLE_0:def 3;
hence a < b by A10, A4; :: 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 A11: ( a in {x} & b in R_ z ) ; :: thesis: not a >= b
then ( b in R_ x or b in R_ y ) by A2, XBOOLE_0:def 3;
hence a < b by A3, A11, A1; :: thesis: verum

end;

hence x == z by A7, A5, SURREAL0:43, A9; :: thesis: verum