let Al be QC-alphabet ; for PHI being Consistent Subset of (CQC-WFF Al)
for Al2 being Al -expanding QC-alphabet
for THETA being Subset of (CQC-WFF Al2) st PHI c= THETA holds
for A2 being non empty set
for J2 being interpretation of Al2,A2
for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
let PHI be Consistent Subset of (CQC-WFF Al); for Al2 being Al -expanding QC-alphabet
for THETA being Subset of (CQC-WFF Al2) st PHI c= THETA holds
for A2 being non empty set
for J2 being interpretation of Al2,A2
for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
let Al2 be Al -expanding QC-alphabet ; for THETA being Subset of (CQC-WFF Al2) st PHI c= THETA holds
for A2 being non empty set
for J2 being interpretation of Al2,A2
for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
let THETA be Subset of (CQC-WFF Al2); ( PHI c= THETA implies for A2 being non empty set
for J2 being interpretation of Al2,A2
for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI )
assume A1:
PHI c= THETA
; for A2 being non empty set
for J2 being interpretation of Al2,A2
for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
let A2 be non empty set ; for J2 being interpretation of Al2,A2
for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
let J2 be interpretation of Al2,A2; for v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA holds
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
let v2 be Element of Valuations_in (Al2,A2); ( J2,v2 |= THETA implies ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI )
assume A2:
J2,v2 |= THETA
; ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
set A = A2;
A3:
QC-pred_symbols Al c= QC-pred_symbols Al2
by Th3;
set Jp = J2 | (QC-pred_symbols Al);
reconsider Jp = J2 | (QC-pred_symbols Al) as Function of (QC-pred_symbols Al),(relations_on A2) by A3, FUNCT_2:32;
for P being Element of QC-pred_symbols Al
for r being Element of relations_on A2 holds
( not Jp . P = r or r = empty_rel A2 or the_arity_of P = the_arity_of r )
then reconsider Jp = Jp as interpretation of Al,A2 by VALUAT_1:def 5;
A7:
bound_QC-variables Al c= bound_QC-variables Al2
by Th4;
set vp = v2 | (bound_QC-variables Al);
reconsider vp = v2 | (bound_QC-variables Al) as Function of (bound_QC-variables Al),A2 by A7, FUNCT_2:32;
A8:
Funcs ((bound_QC-variables Al),A2) = Valuations_in (Al,A2)
by VALUAT_1:def 1;
reconsider vp = vp as Element of Valuations_in (Al,A2) by A8, FUNCT_2:8;
for r being Element of CQC-WFF Al st r in PHI holds
Jp,vp |= r
hence
ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PHI
by CALCUL_1:def 11; verum