let A be QC-alphabet ; :: thesis: for s, t, v being QC-symbol of A st s <= t & t < v holds
s < v
let s, t, v be QC-symbol of A; :: thesis: ( s <= t & t < v implies s < v )
assume A1: ( s <= t & t < v ) ; :: thesis: s < v
then ( s <= t & t <= v ) by Def34;
then A2: s <= v by Th21;
not s = v by A1, Th25;
hence s < v by A2, Def34; :: thesis: verum