let x1, x2, y1, y2 be real number ; :: 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: y2 is Real by XREAL_0:def 1;
y1 is Real by XREAL_0:def 1;
then A10: abs ((a `2) - (b `2)) <= y2 - y1 by A3, A4, A7, A8, A9, JGRAPH_1:27;
A11: ((a `1) - (b `1)) ^2 >= 0 by XREAL_1:63;
A12: ((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 Th101;
then dist (a,b) <= (sqrt (((a `1) - (b `1)) ^2)) + (sqrt (((a `2) - (b `2)) ^2)) by A11, A12, Th6;
then dist (a,b) <= (abs ((a `1) - (b `1))) + (sqrt (((a `2) - (b `2)) ^2)) by COMPLEX1:72;
then A13: dist (a,b) <= (abs ((a `1) - (b `1))) + (abs ((a `2) - (b `2))) by COMPLEX1:72;
A14: x2 is Real by XREAL_0:def 1;
x1 is Real by XREAL_0:def 1;
then abs ((a `1) - (b `1)) <= x2 - x1 by A1, A2, A5, A6, A14, JGRAPH_1:27;
then (abs ((a `1) - (b `1))) + (abs ((a `2) - (b `2))) <= (x2 - x1) + (y2 - y1) by A10, XREAL_1:7;
hence dist (a,b) <= (x2 - x1) + (y2 - y1) by A13, XXREAL_0:2; :: thesis: verum