for Al being QC-alphabet
for A being non empty set
for x being set st x is Element of Valuations_in (Al,A) holds
x is Function of (bound_QC-variables Al),A