let x be Surreal; :: thesis: ( L_ x << {x} & {x} << R_ x )
thus L_ x << {x} :: thesis: {x} << R_ x

proof

let xl, X be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not xl in L_ x or not X in {x} or not xl >= X )
assume A1: ( xl in L_ x & X in {x} & xl >= X ) ; :: thesis: contradiction
xl >= x by A1, TARSKI:def 1;
then ( L_ x << {xl} & xl in {xl} ) by SURREAL0:43, TARSKI:def 1;
then not xl <= xl by A1;
hence contradiction ; :: thesis: verum

end;

let X, xr be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not X in {x} or not xr in R_ x or not X >= xr )
assume A2: ( X in {x} & xr in R_ x & X >= xr ) ; :: thesis: contradiction
xr <= x by A2, TARSKI:def 1;
then ( {xr} << R_ x & xr in {xr} ) by SURREAL0:43, TARSKI:def 1;
then not xr <= xr by A2;
hence contradiction ; :: thesis: verum