theorem Th70: :: INTPRO_1:70

for X being Subset of MC-wff
for p, q being Element of MC-wff st p in CnCPC X & p => q in CnCPC X holds
q in CnCPC X