:: deftheorem defines 'equiv' INTPRO_2:def 1 :
for p, q being Element of MC-wff holds p 'equiv' q = (p => q) '&' (q => p);