let A be QC-alphabet ; :: thesis: for s, t, u being QC-symbol of A st s <= t & t <= u holds
s <= u
let s, t, u be QC-symbol of A; :: thesis: ( s <= t & t <= u implies s <= u )
set R = the Relation of A;
the Relation of A well_orders (QC-symbols A) \ NAT by Def32;
then A1: the Relation of A is_transitive_in (QC-symbols A) \ NAT by WELLORD1:def 5;
assume A2: ( s <= t & t <= u ) ; :: thesis: s <= u

per cases ( s in NAT or not s in NAT ) ;

suppose A3: s in NAT ; :: thesis: s <= u

then A4: t in NAT by A2, Def33;
then A5: u in NAT by A2, Def33;
consider m, n being Nat such that
A6: ( s = m & t = n & m <= n ) by A2, A3, A4, Def33;
consider k, j being Nat such that
A7: ( t = k & u = j & k <= j ) by A2, A4, A5, Def33;
m <= j by A6, A7, XXREAL_0:2;
hence s <= u by A6, A7, Def33, A3, A5; :: thesis: verum

end;

suppose A8: not s in NAT ; :: thesis: s <= u

per cases ( t in NAT or not t in NAT ) ;

suppose t in NAT ; :: thesis: s <= u

then u in NAT by A2, Def33;
hence s <= u by A8, Def33; :: thesis: verum

end;

suppose A9: not t in NAT ; :: thesis: s <= u

per cases ( u in NAT or not u in NAT ) ;

suppose u in NAT ; :: thesis: s <= u

hence s <= u by A8, Def33; :: thesis: verum

end;

suppose A10: not u in NAT ; :: thesis: s <= u

then A11: ( s in (QC-symbols A) \ NAT & t in (QC-symbols A) \ NAT & u in (QC-symbols A) \ NAT ) by A8, A9, XBOOLE_0:def 5;
( [s,t] in the Relation of A & [t,u] in the Relation of A ) by A2, A8, A9, A10, Def33;
then [s,u] in the Relation of A by A1, A11, RELAT_2:def 8;
hence s <= u by A8, A10, Def33; :: thesis: verum

end;

end;

end;

end;

end;

end;