theorem Th85: :: INTPRO_2:84

for p being Element of MC-wff holds |-_IPC p => p