theorem Th116: :: INTPRO_2:115

for X being Subset of MC-wff
for q, r being Element of MC-wff st X |-_IPC r & X \/ {r} |-_IPC q holds
X |-_IPC q