theorem Th7: :: INTPRO_1:7

for X being Subset of MC-wff
for p, q being Element of MC-wff holds q => (p 'or' q) in CnIPC X