for T being Subset of MC-wff holds
( T is IPC_theory iff CnIPC T = T )