:: deftheorem Def3 defines <=_ SURREALO:def 3 :
for X, Y being set holds
( X <=_ Y iff for x being Surreal st x in X holds
ex y1, y2 being Surreal st
( y1 in Y & y2 in Y & y1 <= x & x <= y2 ) );