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 A1: ( x1 <= a `1 & a `1 <= x2 & y1 <= a `2 & a `2 <= y2 & x1 <= b `1 & b `1 <= x2 & y1 <= b `2 & b `2 <= y2 ) ; :: thesis: dist a,b <= (x2 - x1) + (y2 - y1)
A2: dist a,b = sqrt ((((a `1 ) - (b `1 )) ^2 ) + (((a `2 ) - (b `2 )) ^2 )) by Th101;
( x1 is Real & x2 is Real & y1 is Real & y2 is Real ) by XREAL_0:def 1;
then ( abs ((a `1 ) - (b `1 )) <= x2 - x1 & abs ((a `2 ) - (b `2 )) <= y2 - y1 ) by A1, JGRAPH_1:31;
then A3: (abs ((a `1 ) - (b `1 ))) + (abs ((a `2 ) - (b `2 ))) <= (x2 - x1) + (y2 - y1) by XREAL_1:9;
( ((a `1 ) - (b `1 )) ^2 >= 0 & ((a `2 ) - (b `2 )) ^2 >= 0 ) by XREAL_1:65;
then dist a,b <= (sqrt (((a `1 ) - (b `1 )) ^2 )) + (sqrt (((a `2 ) - (b `2 )) ^2 )) by A2, Th6;
then dist a,b <= (abs ((a `1 ) - (b `1 ))) + (sqrt (((a `2 ) - (b `2 )) ^2 )) by COMPLEX1:158;
then dist a,b <= (abs ((a `1 ) - (b `1 ))) + (abs ((a `2 ) - (b `2 ))) by COMPLEX1:158;
hence dist a,b <= (x2 - x1) + (y2 - y1) by A3, XXREAL_0:2; :: thesis: verum