for X being Subset of MC-wff holds X c= CnS4 X