theorem Th12: :: INTPRO_2:11

for X being Subset of MC-wff
for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X holds
Effect_IPC f in CnIPC X