for Al being QC-alphabet
for A being Subset of (bound_QC-variables Al) st A is finite holds
ex x being bound_QC-variable of Al st not x in A