:: deftheorem defines QC-symbols QC_LANG1:def 2 :
for A being QC-alphabet holds QC-symbols A = rng A;