theorem :: QC_LANG1:31

for A being QC-alphabet
for n being Nat
for t being QC-symbol of A holds t <= t + n