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 ) } c= CnIPC X
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { 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 ) } or a in CnIPC X )
assume a in { 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 ) } ; :: thesis: a in CnIPC X
then ex q being Element of MC-wff st
( q = a & ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = q ) ) ;
hence a in CnIPC X by Th12; :: thesis: verum