:: deftheorem defines <= SURREAL0:def 1 :
for a, b being object
for O being set holds
( a <= O,b iff [a,b] in O );