let X be Subset of MC-wff; :: thesis: for p being Element of MC-wff holds
( p in CnIPC X iff ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) )
let p be Element of MC-wff ; :: thesis: ( p in CnIPC X iff ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) )
thus ( p in CnIPC X implies ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) ) :: thesis: ( ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) implies p in CnIPC X )

proof

assume p in CnIPC X ; :: thesis: ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p )
then p in { F where F 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 = F ) } by Th15;
then ex F being Element of MC-wff st
( F = p & ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = F ) ) ;
hence ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) ; :: thesis: verum

end;

given f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] such that A1: ( f is_a_proof_wrt_IPC X & Effect_IPC f = p ) ; :: thesis: p in CnIPC X
p in { F where F 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 = F ) } by A1;
hence p in CnIPC X by Th15; :: thesis: verum