:: deftheorem Def11 defines uniq-surreal SURREALO:def 11 :
for x being Surreal holds
( x is uniq-surreal iff x = Unique_No x );