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