:: deftheorem defines a. QC_LANG3:def 3 :
for A being QC-alphabet
for k being Nat holds A a. k = [6,k];