theorem :: VALUAT_1:16

for Al being QC-alphabet
for k being Nat
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al holds
( J,v |= P ! ll iff (ll 'in' (J . P)) . v = TRUE ) by Lm1;