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