:: deftheorem defines bound_QC-variables QC_LANG1:def 4 :
for A being QC-alphabet holds bound_QC-variables A = [:{4},(QC-symbols A):];