let X be Subset of MC-wff; :: thesis: CnS4 (CnS4 X) = CnS4 X
A1: CnS4 X c= CnS4 (CnS4 X) by Th89;
CnS4 (CnS4 X) c= CnS4 X by Lm23;
hence CnS4 (CnS4 X) = CnS4 X by A1, XBOOLE_0:def 10; :: thesis: verum