let Al be QC-alphabet ; 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); ( PHI c= THETA & PHI is with_examples implies THETA is with_examples )
assume A1:
( PHI c= THETA & PHI is with_examples )
; THETA is with_examples
now 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;
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;
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;
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;
verum end;
hence
THETA is with_examples
by GOEDELCP:def 2; verum