for A being QC-alphabet
for s, t being QC-symbol of A holds
( s < t iff not t <= s ) by Th23, Th24;