let k be Element of NAT ; :: thesis: for A being non empty set
for J being interpretation of A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of
for v, w being Element of Valuations_in 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 A
for P being QC-pred_symbol of k
for ll being CQC-variable_list of
for v, w being Element of Valuations_in 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 A; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of
for v, w being Element of Valuations_in 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; :: thesis: for ll being CQC-variable_list of
for v, w being Element of Valuations_in 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 ; :: thesis: for v, w being Element of Valuations_in 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 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:9;
A3: ( (Valid (P ! ll),J) . v = TRUE iff v *' ll in J . P ) by VALUAT_1:16;
A4: ( ll * (w | (still_not-bound_in ll)) in J . P iff w *' ll in J . P ) by Th60;
( w *' ll in J . P iff (Valid (P ! ll),J) . w = TRUE ) by VALUAT_1:16;
hence ( J,v |= P ! ll iff J,w |= P ! ll ) by A1, A2, A3, A4, Th60, VALUAT_1:def 12; :: thesis: verum