theorem Th11: :: INTPRO_1:11

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