theorem Th29: :: QC_LANG1:29

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;