let Al be QC-alphabet ; :: thesis: 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); :: thesis: 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 ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 )

proof

let P be Element of QC-pred_symbols Al; :: thesis: 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 )
let r be Element of relations_on A2; :: thesis: ( not Jp . P = r or r = empty_rel A2 or the_arity_of P = the_arity_of r )
assume A4: Jp . P = r ; :: thesis: ( r = empty_rel A2 or the_arity_of P = the_arity_of r )
P is Element of QC-pred_symbols Al2 by Th3, TARSKI:def 3;
then consider Q being Element of QC-pred_symbols Al2 such that
A5: P = Q ;
A6: ( P `1 = 7 + (the_arity_of P) & Q `1 = 7 + (the_arity_of Q) ) by QC_LANG1:def 8;
Jp . P = J2 . Q by A5, FUNCT_1:49;
hence ( r = empty_rel A2 or the_arity_of P = the_arity_of r ) by A4, A5, A6, VALUAT_1:def 5; :: thesis: verum

end;

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

proof

let r be Element of CQC-WFF Al; :: thesis: ( r in PHI implies Jp,vp |= r )
assume A9: r in PHI ; :: thesis: Jp,vp |= r
J2,v2 |= Al2 -Cast r by A1, A2, A9, CALCUL_1:def 11;
hence Jp,vp |= r by Th9; :: thesis: verum

end;

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; :: thesis: verum