:: deftheorem defines 0 ORDINAL1:def 13 :
0 = {} ;