theorem Th24: :: INTPRO_2:23

for X being Subset of MC-wff
for p, q being Element of MC-wff holds X |-_IPC q => (p 'or' q) by INTPRO_1:7;