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_{1}[ 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_{1}[p] } c= CQC-WFF Al
from FRAENKEL:sch 10(); :: thesis: verum

( 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

( f is_a_proof_wrt X & Effect f = $1 );

thus { p where p is Element of CQC-WFF Al : S