:: deftheorem Def7 defines |= VALUAT_1:def 7 :
for Al being QC-alphabet
for A being non empty set
for p being Element of CQC-WFF Al
for J being interpretation of Al,A
for v being Element of Valuations_in (Al,A) holds
( J,v |= p iff (Valid (p,J)) . v = TRUE );