:: deftheorem defines 0 QC_LANG1:def 36 :
for A being QC-alphabet
for b₂ being QC-symbol of A holds
( b₂ = 0 A iff for t being QC-symbol of A holds b₂ <= t );