:: deftheorem defines QC-variables QC_LANG1:def 3 :
for A being QC-alphabet holds QC-variables A = [:{6},NAT:] \/ [:{4,5},(QC-symbols A):];