theorem Th101: :: INTPRO_2:100

for p being Element of MC-wff holds |-_IPC FALSUM 'equiv' (p '&' (p => FALSUM))