theorem Th85: :: INTPRO_1:85

for X being Subset of MC-wff
for p being Element of MC-wff holds (Nes p) => p in CnS4 X