let X be Subset of MC-wff; :: thesis: CnCPC (CnCPC X) = CnCPC X
A1: CnCPC X c= CnCPC (CnCPC X) by Th72;
CnCPC (CnCPC X) c= CnCPC X by Lm21;
hence CnCPC (CnCPC X) = CnCPC X by A1, XBOOLE_0:def 10; :: thesis: verum