let Al be QC-alphabet ; :: thesis: for PHI, THETA being Consistent Subset of (CQC-WFF Al) st PHI c= THETA & PHI is with_examples holds
THETA is with_examples
let PHI, THETA be Consistent Subset of (CQC-WFF Al); :: thesis: ( PHI c= THETA & PHI is with_examples implies THETA is with_examples )
assume A1: ( PHI c= THETA & PHI is with_examples ) ; :: thesis: THETA is with_examples

now :: thesis: for x being bound_QC-variable of Al
for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st THETA |- ('not' (Ex (x,p))) 'or' (p . (x,y))

let x be bound_QC-variable of Al; :: thesis: for p being Element of CQC-WFF Al ex y being bound_QC-variable of Al st THETA |- ('not' (Ex (x,p))) 'or' (p . (x,y))
let p be Element of CQC-WFF Al; :: thesis: ex y being bound_QC-variable of Al st THETA |- ('not' (Ex (x,p))) 'or' (p . (x,y))
consider y being bound_QC-variable of Al such that
A2: PHI |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A1, GOEDELCP:def 2;
consider f being FinSequence of CQC-WFF Al such that
A3: ( rng f c= PHI & |- f ^ <*(('not' (Ex (x,p))) 'or' (p . (x,y)))*> ) by A2, HENMODEL:def 1;
take y = y; :: thesis: THETA |- ('not' (Ex (x,p))) 'or' (p . (x,y))
thus THETA |- ('not' (Ex (x,p))) 'or' (p . (x,y)) by A1, A3, HENMODEL:def 1, XBOOLE_1:1; :: thesis: verum

end;

hence THETA is with_examples by GOEDELCP:def 2; :: thesis: verum