let n be Element of NAT ; :: thesis: for p, q, r being Element of n -tuples_on NAT holds
( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )

let p, q, r be Element of n -tuples_on NAT; :: thesis: ( ( p < q & q < r implies p < r ) & ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r ) )
thus A1: ( p < q & q < r implies p < r ) :: thesis: ( ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) implies p <= r )
proof
assume that
A2: p < q and
A3: q < r ; :: thesis: p < r
consider i being Element of NAT such that
A4: i in Seg n and
A5: p . i < q . i and
A6: for k being Nat st 1 <= k & k < i holds
p . k = q . k by A2;
consider j being Element of NAT such that
A7: j in Seg n and
A8: q . j < r . j and
A9: for k being Nat st 1 <= k & k < j holds
q . k = r . k by A3;
reconsider t = min (i,j) as Element of NAT ;
take t ; :: according to POLYNOM3:def 1 :: thesis: ( t in Seg n & p . t < r . t & ( for k being Nat st 1 <= k & k < t holds
p . k = r . k ) )

thus t in Seg n by ; :: thesis: ( p . t < r . t & ( for k being Nat st 1 <= k & k < t holds
p . k = r . k ) )

now :: thesis: p . t < r . t
per cases ( i < j or i > j or i = j ) by XXREAL_0:1;
suppose A10: i < j ; :: thesis: p . t < r . t
A11: i >= 1 by ;
t = i by ;
hence p . t < r . t by A5, A9, A10, A11; :: thesis: verum
end;
suppose A12: i > j ; :: thesis: p . t < r . t
A13: j >= 1 by ;
t = j by ;
hence p . t < r . t by A6, A8, A12, A13; :: thesis: verum
end;
suppose i = j ; :: thesis: p . t < r . t
hence p . t < r . t by ; :: thesis: verum
end;
end;
end;
hence p . t < r . t ; :: thesis: for k being Nat st 1 <= k & k < t holds
p . k = r . k

let k be Nat; :: thesis: ( 1 <= k & k < t implies p . k = r . k )
assume that
A14: 1 <= k and
A15: k < t ; :: thesis: p . k = r . k
t <= j by XXREAL_0:17;
then A16: k < j by ;
t <= i by XXREAL_0:17;
then k < i by ;
hence p . k = q . k by
.= r . k by A9, A14, A16 ;
:: thesis: verum
end;
assume A17: ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) ; :: thesis: p <= r
per cases ( ( p < q & q <= r ) or ( p <= q & q < r ) or ( p <= q & q <= r ) ) by A17;
suppose A18: ( p < q & q <= r ) ; :: thesis: p <= r
thus p <= r by ; :: thesis: verum
end;
suppose A19: ( p <= q & q < r ) ; :: thesis: p <= r
thus p <= r by ; :: thesis: verum
end;
suppose ( p <= q & q <= r ) ; :: thesis: p <= r
hence p <= r by A1; :: thesis: verum
end;
end;