theorem Th8: :: VALUAT_1:8

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 p being Element of CQC-WFF Al
for J being interpretation of Al,A
for P being QC-pred_symbol of k,Al
for r being Element of relations_on A st p = P ! ll & r = J . P holds
( not v *' ll in r iff (Valid (p,J)) . v = FALSE )