theorem :: INTPRO_2:67

for X being Subset of MC-wff
for p being Element of MC-wff st p in X holds
p in CnIPC X