theorem Th45: :: INTPRO_2:44

for p, q being Element of MC-wff holds q => (p 'or' q) is valid_IPC