:: deftheorem defines x. QC_LANG3:def 2 :
for A being QC-alphabet
for s being QC-symbol of A holds x. s = [4,s];