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