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 = THETA holds

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

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 = THETA holds

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let Al2 be Al -expanding QC-alphabet ; :: thesis: for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let THETA be Subset of (CQC-WFF Al2); :: thesis: ( PHI = THETA implies for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA )

assume A1: PHI = THETA ; :: thesis: for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let A be non empty set ; :: thesis: for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= PHI implies ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA )

assume A2: J,v |= PHI ; :: thesis: ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

set J2 = ((QC-pred_symbols Al2) --> (empty_rel A)) +* J;

A3: ( dom J = QC-pred_symbols Al & dom ((QC-pred_symbols Al2) --> (empty_rel A)) = QC-pred_symbols Al2 ) by FUNCT_2:def 1;

then dom (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) = (QC-pred_symbols Al) \/ (QC-pred_symbols Al2) by FUNCT_4:def 1;

then A4: dom (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) = QC-pred_symbols Al2 by Th3, XBOOLE_1:12;

J in Funcs ((QC-pred_symbols Al),(relations_on A)) by FUNCT_2:8;

then rng J c= relations_on A by FUNCT_2:92;

then ( (rng ((QC-pred_symbols Al2) --> (empty_rel A))) \/ (rng J) c= relations_on A & rng (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) c= (rng ((QC-pred_symbols Al2) --> (empty_rel A))) \/ (rng J) ) by FUNCT_4:17, XBOOLE_1:8;

then reconsider J2 = ((QC-pred_symbols Al2) --> (empty_rel A)) +* J as Function of (QC-pred_symbols Al2),(relations_on A) by A4, FUNCT_2:2, XBOOLE_1:1;

A5: J = J2 | (QC-pred_symbols Al) by A3, FUNCT_4:23;

for P2 being Element of QC-pred_symbols Al2

for r being Element of relations_on A holds

( not J2 . P2 = r or r = empty_rel A or the_arity_of P2 = the_arity_of r )

set a = the Element of A;

set v2 = ((bound_QC-variables Al2) --> the Element of A) +* v;

v in Valuations_in (Al,A) ;

then v in Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then A9: ( dom v = bound_QC-variables Al & dom ((bound_QC-variables Al2) --> the Element of A) = bound_QC-variables Al2 ) by FUNCT_2:92;

then dom (((bound_QC-variables Al2) --> the Element of A) +* v) = (bound_QC-variables Al) \/ (bound_QC-variables Al2) by FUNCT_4:def 1;

then A10: dom (((bound_QC-variables Al2) --> the Element of A) +* v) = bound_QC-variables Al2 by Th4, XBOOLE_1:12;

v in Valuations_in (Al,A) ;

then v in Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then rng v c= A by FUNCT_2:92;

then ( (rng ((bound_QC-variables Al2) --> the Element of A)) \/ (rng v) c= A & rng (((bound_QC-variables Al2) --> the Element of A) +* v) c= (rng ((bound_QC-variables Al2) --> the Element of A)) \/ (rng v) ) by FUNCT_4:17, XBOOLE_1:8;

then reconsider v2 = ((bound_QC-variables Al2) --> the Element of A) +* v as Function of (bound_QC-variables Al2),A by A10, FUNCT_2:2, XBOOLE_1:1;

A11: v = v2 | (bound_QC-variables Al) by A9, FUNCT_4:23;

v2 in Funcs ((bound_QC-variables Al2),A) by FUNCT_2:8;

then reconsider v2 = v2 as Element of Valuations_in (Al2,A) by VALUAT_1:def 1;

for p2 being Element of CQC-WFF Al2 st p2 in THETA holds

J2,v2 |= p2

for Al2 being Al -expanding QC-alphabet

for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

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 = THETA holds

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let Al2 be Al -expanding QC-alphabet ; :: thesis: for THETA being Subset of (CQC-WFF Al2) st PHI = THETA holds

for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let THETA be Subset of (CQC-WFF Al2); :: thesis: ( PHI = THETA implies for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA )

assume A1: PHI = THETA ; :: thesis: for A being non empty set

for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let A be non empty set ; :: thesis: for J being interpretation of Al,A

for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let J be interpretation of Al,A; :: thesis: for v being Element of Valuations_in (Al,A) st J,v |= PHI holds

ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

let v be Element of Valuations_in (Al,A); :: thesis: ( J,v |= PHI implies ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA )

assume A2: J,v |= PHI ; :: thesis: ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA

set J2 = ((QC-pred_symbols Al2) --> (empty_rel A)) +* J;

A3: ( dom J = QC-pred_symbols Al & dom ((QC-pred_symbols Al2) --> (empty_rel A)) = QC-pred_symbols Al2 ) by FUNCT_2:def 1;

then dom (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) = (QC-pred_symbols Al) \/ (QC-pred_symbols Al2) by FUNCT_4:def 1;

then A4: dom (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) = QC-pred_symbols Al2 by Th3, XBOOLE_1:12;

J in Funcs ((QC-pred_symbols Al),(relations_on A)) by FUNCT_2:8;

then rng J c= relations_on A by FUNCT_2:92;

then ( (rng ((QC-pred_symbols Al2) --> (empty_rel A))) \/ (rng J) c= relations_on A & rng (((QC-pred_symbols Al2) --> (empty_rel A)) +* J) c= (rng ((QC-pred_symbols Al2) --> (empty_rel A))) \/ (rng J) ) by FUNCT_4:17, XBOOLE_1:8;

then reconsider J2 = ((QC-pred_symbols Al2) --> (empty_rel A)) +* J as Function of (QC-pred_symbols Al2),(relations_on A) by A4, FUNCT_2:2, XBOOLE_1:1;

A5: J = J2 | (QC-pred_symbols Al) by A3, FUNCT_4:23;

for P2 being Element of QC-pred_symbols Al2

for r being Element of relations_on A holds

( not J2 . P2 = r or r = empty_rel A or the_arity_of P2 = the_arity_of r )

proof

then reconsider J2 = J2 as interpretation of Al2,A by VALUAT_1:def 5;
let P2 be Element of QC-pred_symbols Al2; :: thesis: for r being Element of relations_on A holds

( not J2 . P2 = r or r = empty_rel A or the_arity_of P2 = the_arity_of r )

let r be Element of relations_on A; :: thesis: ( not J2 . P2 = r or r = empty_rel A or the_arity_of P2 = the_arity_of r )

assume A6: J2 . P2 = r ; :: thesis: ( r = empty_rel A or the_arity_of P2 = the_arity_of r )

end;( not J2 . P2 = r or r = empty_rel A or the_arity_of P2 = the_arity_of r )

let r be Element of relations_on A; :: thesis: ( not J2 . P2 = r or r = empty_rel A or the_arity_of P2 = the_arity_of r )

assume A6: J2 . P2 = r ; :: thesis: ( r = empty_rel A or the_arity_of P2 = the_arity_of r )

per cases
( P2 in QC-pred_symbols Al or not P2 in QC-pred_symbols Al )
;

end;

suppose
P2 in QC-pred_symbols Al
; :: thesis: ( r = empty_rel A or the_arity_of P2 = the_arity_of r )

then consider P being QC-pred_symbol of Al such that

A7: P = P2 ;

A8: J . P = r by A3, A6, A7, FUNCT_4:13;

7 + (the_arity_of P2) = P `1 by A7, QC_LANG1:def 8

.= 7 + (the_arity_of P) by QC_LANG1:def 8 ;

hence ( r = empty_rel A or the_arity_of P2 = the_arity_of r ) by A8, VALUAT_1:def 5; :: thesis: verum

end;A7: P = P2 ;

A8: J . P = r by A3, A6, A7, FUNCT_4:13;

7 + (the_arity_of P2) = P `1 by A7, QC_LANG1:def 8

.= 7 + (the_arity_of P) by QC_LANG1:def 8 ;

hence ( r = empty_rel A or the_arity_of P2 = the_arity_of r ) by A8, VALUAT_1:def 5; :: thesis: verum

suppose
not P2 in QC-pred_symbols Al
; :: thesis: ( r = empty_rel A or the_arity_of P2 = the_arity_of r )

then
not P2 in dom J
by FUNCT_2:def 1;

then J2 . P2 = ((QC-pred_symbols Al2) --> (empty_rel A)) . P2 by FUNCT_4:11

.= empty_rel A ;

hence ( r = empty_rel A or the_arity_of P2 = the_arity_of r ) by A6; :: thesis: verum

end;then J2 . P2 = ((QC-pred_symbols Al2) --> (empty_rel A)) . P2 by FUNCT_4:11

.= empty_rel A ;

hence ( r = empty_rel A or the_arity_of P2 = the_arity_of r ) by A6; :: thesis: verum

set a = the Element of A;

set v2 = ((bound_QC-variables Al2) --> the Element of A) +* v;

v in Valuations_in (Al,A) ;

then v in Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then A9: ( dom v = bound_QC-variables Al & dom ((bound_QC-variables Al2) --> the Element of A) = bound_QC-variables Al2 ) by FUNCT_2:92;

then dom (((bound_QC-variables Al2) --> the Element of A) +* v) = (bound_QC-variables Al) \/ (bound_QC-variables Al2) by FUNCT_4:def 1;

then A10: dom (((bound_QC-variables Al2) --> the Element of A) +* v) = bound_QC-variables Al2 by Th4, XBOOLE_1:12;

v in Valuations_in (Al,A) ;

then v in Funcs ((bound_QC-variables Al),A) by VALUAT_1:def 1;

then rng v c= A by FUNCT_2:92;

then ( (rng ((bound_QC-variables Al2) --> the Element of A)) \/ (rng v) c= A & rng (((bound_QC-variables Al2) --> the Element of A) +* v) c= (rng ((bound_QC-variables Al2) --> the Element of A)) \/ (rng v) ) by FUNCT_4:17, XBOOLE_1:8;

then reconsider v2 = ((bound_QC-variables Al2) --> the Element of A) +* v as Function of (bound_QC-variables Al2),A by A10, FUNCT_2:2, XBOOLE_1:1;

A11: v = v2 | (bound_QC-variables Al) by A9, FUNCT_4:23;

v2 in Funcs ((bound_QC-variables Al2),A) by FUNCT_2:8;

then reconsider v2 = v2 as Element of Valuations_in (Al2,A) by VALUAT_1:def 1;

for p2 being Element of CQC-WFF Al2 st p2 in THETA holds

J2,v2 |= p2

proof

hence
ex A2 being non empty set ex J2 being interpretation of Al2,A2 ex v2 being Element of Valuations_in (Al2,A2) st J2,v2 |= THETA
by CALCUL_1:def 11; :: thesis: verum
let p2 be Element of CQC-WFF Al2; :: thesis: ( p2 in THETA implies J2,v2 |= p2 )

assume A12: p2 in THETA ; :: thesis: J2,v2 |= p2

consider p being Element of CQC-WFF Al such that

A13: ( p = p2 & p in PHI ) by A1, A12;

J,v |= p by A2, A13, CALCUL_1:def 11;

then J2,v2 |= Al2 -Cast p by A5, A11, Th9;

hence J2,v2 |= p2 by A13; :: thesis: verum

end;assume A12: p2 in THETA ; :: thesis: J2,v2 |= p2

consider p being Element of CQC-WFF Al such that

A13: ( p = p2 & p in PHI ) by A1, A12;

J,v |= p by A2, A13, CALCUL_1:def 11;

then J2,v2 |= Al2 -Cast p by A5, A11, Th9;

hence J2,v2 |= p2 by A13; :: thesis: verum