:: deftheorem defines 1. SUPINF_2:def 14 :
1. = 1;