:: deftheorem Def4 defines 'in' VALUAT_1:def 4 :
for Al being QC-alphabet
for A being non empty set
for k being Nat
for ll being CQC-variable_list of k,Al
for r being Element of relations_on A
for b₆ being Element of Funcs ((Valuations_in (Al,A)),BOOLEAN) holds
( b₆ = ll 'in' r iff for v being Element of Valuations_in (Al,A) holds
( ( v *' ll in r implies b₆ . v = TRUE ) & ( b₆ . v = TRUE implies v *' ll in r ) & ( not v *' ll in r implies b₆ . v = FALSE ) & ( b₆ . v = FALSE implies not v *' ll in r ) ) );