theorem Th86: :: INTPRO_1:86

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