theorem :: INTPRO_2:149

for p being Element of MC-wff holds |-_IPC (p '&' (neg p)) => FALSUM by Th100;