:: deftheorem defines multint0 INT_7:def 3 :
for n being Prime holds multint0 n = (multint n) || (Segm0 n);