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