theorem Th24: :: QC_LANG1:24

for A being QC-alphabet
for t, u being QC-symbol of A holds
( t <= u or u <= t )