theorem Th21: :: QC_LANG1:21

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