theorem :: INTPRO_2:129

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