let x, y be Surreal; :: thesis: ( x == y implies {x} <=_ {y} )
assume A1: x == y ; :: thesis: {x} <=_ {y}
let z be Surreal; :: according to SURREALO:def 3 :: thesis: ( z in {x} implies ex y1, y2 being Surreal st
( y1 in {y} & y2 in {y} & y1 <= z & z <= y2 ) )
assume A2: z in {x} ; :: thesis: ex y1, y2 being Surreal st
( y1 in {y} & y2 in {y} & y1 <= z & z <= y2 )
take y ; :: thesis: ex y2 being Surreal st
( y in {y} & y2 in {y} & y <= z & z <= y2 )
take y ; :: thesis: ( y in {y} & y in {y} & y <= z & z <= y )
thus ( y in {y} & y in {y} & y <= z & z <= y ) by A1, A2, TARSKI:def 1; :: thesis: verum