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 | ();
reconsider Jp = J2 | () as Function of (),() by ;
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 ;
then consider Q being Element of QC-pred_symbols Al2 such that
A5: P = Q ;
A6: ( P `1 = 7 + () & Q `1 = 7 + () ) by QC_LANG1:def 8;
Jp . P = J2 . Q by ;
hence ( r = empty_rel A2 or the_arity_of P = the_arity_of r ) by ; :: 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 | ();
reconsider vp = v2 | () as Function of (),A2 by ;
A8: Funcs ((),A2) = Valuations_in (Al,A2) by VALUAT_1:def 1;
reconsider vp = vp as Element of Valuations_in (Al,A2) by ;
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 ;
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