let X be Subset of CQC-WFF; :: thesis: { p where p is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = p ) } c= CQC-WFF
defpred S₁[ set ] means ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = $1 );
thus { p where p is Element of CQC-WFF : S₁[p] } c= CQC-WFF from FRAENKEL:sch 10(); :: thesis: verum