theorem Th14: :: INTPRO_2:13

for Y, X being Subset of MC-wff st Y = { p where p is Element of MC-wff : ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) } holds
Y is IPC_theory by Lm2, Lm3, Lm4, Lm5, Lm6, Lm7, Lm8, Lm9, Lm10, Lm11;