:: deftheorem defines 0_No SURREAL0:def 15 :
0_No = [{},{}];