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

hereby :: thesis: ( CnIPC T = T implies T is IPC_theory )

assume A1: T is IPC_theory ; :: thesis: CnIPC T = T
A2: CnIPC T c= T by A1, Def15;
T c= CnIPC T by Th12;
hence CnIPC T = T by A2, XBOOLE_0:def 10; :: thesis: verum

end;

thus ( CnIPC T = T implies T is IPC_theory ) ; :: thesis: verum