for Al being QC-alphabet
for x being bound_QC-variable of Al
for S being Element of CQC-Sub-WFF Al st x in dom (@ (S `2)) holds
(@ (S `2)) . x is bound_QC-variable of Al