for A being QC-alphabet
for s, t, v being QC-symbol of A st s <= t & t < v holds
s < v by Th21, Th25;