let T be Subset of MC-wff; :: thesis: ( T is CPC_theory iff CnCPC T = T )

hereby :: thesis: ( CnCPC T = T implies T is CPC_theory )

assume A1: T is CPC_theory ; :: thesis: CnCPC T = T
A2: CnCPC T c= T by A1, Def20;
T c= CnCPC T by Th72;
hence CnCPC T = T by A2, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( CnCPC T = T implies T is CPC_theory ) ; :: thesis: verum