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