:: deftheorem defines => INTPRO_1:def 10 :
for p, q being Element of MC-wff holds p => q = (<*1*> ^ p) ^ q;