theorem Th23: :: QC_LANG1:23

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