theorem Th60: :: SUBLEMMA:60

for Al being QC-alphabet
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 )