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