let x, y, z be Surreal; :: thesis: ( x == y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] implies x == z )
assume A1: ( x == y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] ) ; :: thesis: x == z
( L_ y << {y} & {y} << R_ y ) by Th11;
then ( L_ y << {x} & {x} << R_ y ) by A1, Th17, Th18;
hence x == z by A1, Th15; :: thesis: verum