let x, y be Surreal; :: thesis: ( {x} << {y} iff x < y )

hereby :: thesis: ( x < y implies {x} << {y} )

assume A1: {x} << {y} ; :: thesis: x < y
( x in {x} & y in {y} ) by TARSKI:def 1;
hence x < y by A1; :: thesis: verum

end;

assume A2: x < y ; :: thesis: {x} << {y}
let l be Surreal; :: according to SURREAL0:def 20 :: thesis: for b₁ being set holds
( not l in {x} or not b₁ in {y} or not l >= b₁ )
let r be Surreal; :: thesis: ( not l in {x} or not r in {y} or not l >= r )
assume ( l in {x} & r in {y} ) ; :: thesis: not l >= r
then ( l = x & r = y ) by TARSKI:def 1;
hence not l >= r by A2; :: thesis: verum