theorem Th120: :: INTPRO_2:119

for q, r being Element of MC-wff holds {q} |-_IPC q 'or' r