:: deftheorem defines 1_No SURREALO:def 1 :
1_No = [{0_No},{}];