:: deftheorem defines No_omega SURREALC:def 1 :
No_omega = No_uOrdinal_op omega;