:: deftheorem Def14 defines surreal SURREAL0:def 14 :
for o being object holds
( o is surreal iff ex A being Ordinal st o in Day A );