let x be Surreal; :: thesis: ( L_ x <> {x} & {x} <> R_ x )
A1: x in {x} by TARSKI:def 1;
thus L_ x <> {x} :: thesis: {x} <> R_ x

proof

assume L_ x = {x} ; :: thesis: contradiction
then x in (L_ x) \/ (R_ x) by A1, XBOOLE_0:def 3;
then born x in born x by Th1;
hence contradiction ; :: thesis: verum

end;

assume R_ x = {x} ; :: thesis: contradiction
then x in (L_ x) \/ (R_ x) by A1, XBOOLE_0:def 3;
then born x in born x by Th1;
hence contradiction ; :: thesis: verum