let T be Subset of MC-wff; :: thesis: ( T is IPC_theory implies IPC-Taut c= T )
assume A1: T is IPC_theory ; :: thesis: IPC-Taut c= T
IPC-Taut c= CnIPC T by Th13, XBOOLE_1:2;
hence IPC-Taut c= T by A1, Th15; :: thesis: verum