theorem :: QC_LANG1:30

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;