theorem Th15: :: INTPRO_2:14

for X being Subset of MC-wff holds { 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 ) } = CnIPC X