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= MC-wff
defpred S₁[ set ] means ex f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st
( f is_a_proof_wrt_IPC X & Effect_IPC f = $1 );
thus { p where p is Element of MC-wff : S₁[p] } c= MC-wff from FRAENKEL:sch 10(); :: thesis: verum