theorem Th44: :: INTPRO_2:43

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