for T, X being Subset of MC-wff st T is IPC_theory & X c= T holds
CnIPC X c= T by Def15;