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:31;
A11: ((a `1 ) - (b `1 )) ^2 >= 0 by XREAL_1:65;
A12: ((a `2 ) - (b `2 )) ^2 >= 0 by XREAL_1:65;
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:158;
then A13: dist a,b <= (abs ((a `1 ) - (b `1 ))) + (abs ((a `2 ) - (b `2 ))) by COMPLEX1:158;
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:31;
then (abs ((a `1 ) - (b `1 ))) + (abs ((a `2 ) - (b `2 ))) <= (x2 - x1) + (y2 - y1) by A10, XREAL_1:9;
hence dist a,b <= (x2 - x1) + (y2 - y1) by A13, XXREAL_0:2; :: thesis: verum