let n be Element of NAT ; :: thesis:
let p, q, r be Element of n -tuples_on NAT ; :: thesis:
thus A1: ( p < q & q < r implies p < r ) :: thesis:

proof

assume that
A2: p < q and
A3: q < r ; :: thesis:
consider i being Element of NAT such that
A4: i in Seg n and
A5: p . i < q . i and
A6: for k being Element of NAT st 1 <= k & k < i holds
p . k = q . k by A2, Def1;
consider j being Element of NAT such that
A7: j in Seg n and
A8: q . j < r . j and
A9: for k being Element of NAT st 1 <= k & k < j holds
q . k = r . k by A3, Def1;
reconsider t = min i,j as Element of NAT by FINSEQ_2:1;
take t ; :: according to POLYNOM3:def 1 :: thesis:
thus t in Seg n by A4, A7, XXREAL_0:15; :: thesis:

now

per cases by XXREAL_0:1;

suppose A10: i < j ; :: thesis:

A11: i >= 1 by A4, FINSEQ_1:3;
t = i by A10, XXREAL_0:def 9;
hence p . t < r . t by A5, A9, A10, A11; :: thesis:

end;

suppose A12: i > j ; :: thesis:

A13: j >= 1 by A7, FINSEQ_1:3;
t = j by A12, XXREAL_0:def 9;
hence p . t < r . t by A6, A8, A12, A13; :: thesis:

end;

suppose i = j ; :: thesis:

hence p . t < r . t by A5, A8, XXREAL_0:2; :: thesis:

end;

end;

end;

hence p . t < r . t ; :: thesis:
let k be Element of NAT ; :: thesis:
assume that
A14: 1 <= k and
A15: k < t ; :: thesis:
t <= j by XXREAL_0:17;
then A16: k < j by A15, XXREAL_0:2;
t <= i by XXREAL_0:17;
then k < i by A15, XXREAL_0:2;
hence p . k = q . k by A6, A14
.= r . k by A9, A14, A16 ;
:: thesis:

end;

assume A17: ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) ; :: thesis:

per cases by A17;

suppose A18: ( p < q & q <= r ) ; :: thesis:

then ( q < r or q = r ) by Def2;
hence p <= r by A1, A18, Def2; :: thesis:

end;

suppose A19: ( p <= q & q < r ) ; :: thesis:

then ( p < q or p = q ) by Def2;
hence p <= r by A1, A19, Def2; :: thesis:

end;

suppose ( p <= q & q <= r ) ; :: thesis:

hence p <= r by A1, Def2; :: thesis:

end;

end;