for Al being QC-alphabet
for A being non empty set
for J being interpretation of Al,A
for p being Element of CQC-WFF Al
for v, w being Element of Valuations_in (Al,A) st v | (still_not-bound_in p) = w | (still_not-bound_in p) holds
( J,v |= p iff J,w |= p )