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