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 k
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 k
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 k
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 k
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 k; :: 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: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 Th60;
hence ( J,v |= P ! ll iff J,w |= P ! ll ) by A1, A2, A4, A3, Th60, VALUAT_1:def 7; :: thesis: verum