:: deftheorem defines free_QC-variables QC_LANG1:def 6 :
for A being QC-alphabet holds free_QC-variables A = [:{6},NAT:];