for A being QC-alphabet
for t, u being QC-symbol of A st t <= u & u <= t holds
u = t