let Al be QC-alphabet ; :: thesis: for k being Nat
for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) holds
( J,v |= P ! ll iff J,w |= P ! ll )
let k be Nat; :: thesis: for A being non empty set
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) holds
( J,v |= P ! ll iff J,w |= P ! ll )
let A be non empty set ; :: thesis: for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) holds
( J,v |= P ! ll iff J,w |= P ! ll )
let J be interpretation of Al,A; :: thesis: for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) holds
( J,v |= P ! ll iff J,w |= P ! ll )
let P be QC-pred_symbol of k,Al; :: thesis: for ll being CQC-variable_list of k,Al
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) holds
( J,v |= P ! ll iff J,w |= P ! ll )
let ll be CQC-variable_list of k,Al; :: thesis: for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) holds
( J,v |= P ! ll iff J,w |= P ! ll )
let v, w be Element of Valuations_in (Al,A); :: thesis: ( v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) implies ( J,v |= P ! ll iff J,w |= P ! ll ) )
assume A1: v | (still_not-bound_in (P ! ll)) = w | (still_not-bound_in (P ! ll)) ; :: thesis: ( J,v |= P ! ll iff J,w |= P ! ll )
A2: still_not-bound_in (P ! ll) = still_not-bound_in ll by QC_LANG3:5;
A3: ( w *' ll in J . P iff (Valid ((P ! ll),J)) . w = TRUE ) by VALUAT_1:7;
A4: ( (Valid ((P ! ll),J)) . v = TRUE iff v *' ll in J . P ) by VALUAT_1:7;
( ll * (w | (still_not-bound_in ll)) in J . P iff w *' ll in J . P ) by Th59;
hence ( J,v |= P ! ll iff J,w |= P ! ll ) by A1, A2, A4, A3, Th59, VALUAT_1:def 7; :: thesis: verum