let T be Subset of MC-wff; :: thesis: ( T is CPC_theory implies CPC-Taut c= T )
assume A1: T is CPC_theory ; :: thesis: CPC-Taut c= T
CPC-Taut c= CnCPC T by Th73, XBOOLE_1:2;
hence CPC-Taut c= T by A1, Th75; :: thesis: verum