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