let X be Subset of MC-wff ; :: thesis: CnIPC (CnIPC X) = CnIPC X
( CnIPC (CnIPC X) c= CnIPC X & CnIPC X c= CnIPC (CnIPC X) ) by Lm2, Th12;
hence CnIPC (CnIPC X) = CnIPC X by XBOOLE_0:def 10; :: thesis: verum