theorem :: INTPRO_1:91

for X being Subset of MC-wff holds CnS4 (CnS4 X) = CnS4 X