:: deftheorem defines VERUM QC_LANG1:def 14 :
for A being QC-alphabet holds VERUM A = <*[0,0]*>;