theorem :: INTPRO_2:132

for p being Element of MC-wff holds |-_IPC p => (neg (neg (neg (neg p)))) by Th79;