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