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 )

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

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

then reconsider Jp = Jp as interpretation of Al,A2 by VALUAT_1:def 5;
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;( 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

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

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
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;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