:: deftheorem Def12 defines uniq-surreal-membered SURREALO:def 12 :
for X being set holds
( X is uniq-surreal-membered iff for o being object st o in X holds
o is uSurreal );