:: deftheorem defines <= SURREAL0:def 17 :
for x, y being Surreal holds
( x <= y iff ex A being Ordinal st x <= No_Ord A,y );