let X be Subset of MC-wff; :: thesis: { 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
set PX = { 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 ) } ;
A1: { 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 ) } c= CnIPC X by Lm12;
reconsider PX = { 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 ) } as Subset of MC-wff by Lm1;
X c= PX by Th13;
hence { 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 by A1, Th14, INTPRO_1:11; :: thesis: verum