for x1, x2, y1, y2 being Real
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)