let x1, x2, y1, y2 be Real; :: thesis: for a, b being Point of (TOP-REAL 2) st x1 <= a `1 & a `1 <= x2 & y1 <= a `2 & a `2 <= y2 & x1 <= b `1 & b `1 <= x2 & y1 <= b `2 & b `2 <= y2 holds
dist (a,b) <= (x2 - x1) + (y2 - y1)
let a, b be Point of (TOP-REAL 2); :: thesis: ( x1 <= a `1 & a `1 <= x2 & y1 <= a `2 & a `2 <= y2 & x1 <= b `1 & b `1 <= x2 & y1 <= b `2 & b `2 <= y2 implies dist (a,b) <= (x2 - x1) + (y2 - y1) )
assume that
A1: x1 <= a `1 and
A2: a `1 <= x2 and
A3: y1 <= a `2 and
A4: a `2 <= y2 and
A5: x1 <= b `1 and
A6: b `1 <= x2 and
A7: y1 <= b `2 and
A8: b `2 <= y2 ; :: thesis: dist (a,b) <= (x2 - x1) + (y2 - y1)
A9: |.((a `2) - (b `2)).| <= y2 - y1 by A3, A4, A7, A8, JGRAPH_1:27;
A10: ((a `1) - (b `1)) ^2 >= 0 by XREAL_1:63;
A11: ((a `2) - (b `2)) ^2 >= 0 by XREAL_1:63;
dist (a,b) = sqrt ((((a `1) - (b `1)) ^2) + (((a `2) - (b `2)) ^2)) by Th85;
then dist (a,b) <= (sqrt (((a `1) - (b `1)) ^2)) + (sqrt (((a `2) - (b `2)) ^2)) by A10, A11, SQUARE_1:59;
then dist (a,b) <= |.((a `1) - (b `1)).| + (sqrt (((a `2) - (b `2)) ^2)) by COMPLEX1:72;
then A12: dist (a,b) <= |.((a `1) - (b `1)).| + |.((a `2) - (b `2)).| by COMPLEX1:72;
|.((a `1) - (b `1)).| <= x2 - x1 by A1, A2, A5, A6, JGRAPH_1:27;
then |.((a `1) - (b `1)).| + |.((a `2) - (b `2)).| <= (x2 - x1) + (y2 - y1) by A9, XREAL_1:7;
hence dist (a,b) <= (x2 - x1) + (y2 - y1) by A12, XXREAL_0:2; :: thesis: verum