theorem Th23: :: INTPRO_2:22

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