:: deftheorem Def10 defines No_ordinal SURREALN:def 10 :
for x being Surreal holds
( x is No_ordinal iff R_ x = {} );