let A be QC-alphabet ; :: thesis: for s being QC-symbol of A holds s < s ++
let s be QC-symbol of A; :: thesis: s < s ++
s ++ in Seg s by Def35;
then consider t being QC-symbol of A such that
A1: ( t = s ++ & s < t ) ;
thus s < s ++ by A1; :: thesis: verum