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