theorem :: INTPRO_2:123

for Y, X being Subset of MC-wff
for p, q, r being Element of MC-wff st X \/ {p} |-_IPC r & Y \/ {q} |-_IPC r holds
(X \/ Y) \/ {(p 'or' q)} |-_IPC r