:: Compactness of the Bounded Closed Subsets of TOP-REAL 2
:: by Artur Korni{\l}owicz
::
:: Received February 19, 1999
:: Copyright (c) 1999 Association of Mizar Users


begin

theorem :: TOPREAL6:1
canceled;

theorem :: TOPREAL6:2
canceled;

theorem :: TOPREAL6:3
canceled;

theorem :: TOPREAL6:4
canceled;

theorem :: TOPREAL6:5
canceled;

theorem Th6: :: TOPREAL6:6
for a, b being real number st 0 <= a & 0 <= b holds
sqrt (a + b) <= (sqrt a) + (sqrt b)
proof end;

theorem Th7: :: TOPREAL6:7
for a, b being real number st 0 <= a & a <= b holds
abs a <= abs b
proof end;

theorem Th8: :: TOPREAL6:8
for b, a being real number st b <= a & a <= 0 holds
abs a <= abs b
proof end;

theorem :: TOPREAL6:9
for r being Real holds Product (0 |-> r) = 1 by RVSUM_1:124;

theorem Th10: :: TOPREAL6:10
for r being Real holds Product (1 |-> r) = r
proof end;

theorem :: TOPREAL6:11
for r being Real holds Product (2 |-> r) = r * r
proof end;

theorem Th12: :: TOPREAL6:12
for r being Real
for n being Element of NAT holds Product ((n + 1) |-> r) = (Product (n |-> r)) * r
proof end;

theorem Th13: :: TOPREAL6:13
for r being Real
for j being Element of NAT holds
( ( j <> 0 & r = 0 ) iff Product (j |-> r) = 0 )
proof end;

theorem Th14: :: TOPREAL6:14
for r being Real
for j, i being Element of NAT st r <> 0 & j <= i holds
Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r))
proof end;

theorem :: TOPREAL6:15
for r being Real
for j, i being Element of NAT st r <> 0 & j <= i holds
r |^ (i -' j) = (r |^ i) / (r |^ j)
proof end;

theorem Th16: :: TOPREAL6:16
for a, b being Real holds sqr <*a,b*> = <*(a ^2),(b ^2)*>
proof end;

theorem Th17: :: TOPREAL6:17
for a being Real
for i being Nat
for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds
(abs F) . i = abs a
proof end;

theorem :: TOPREAL6:18
for a, b being Real holds abs <*a,b*> = <*(abs a),(abs b)*>
proof end;

theorem :: TOPREAL6:19
for a, b, c, d being real number st a <= b & c <= d holds
(abs (b - a)) + (abs (d - c)) = (b - a) + (d - c)
proof end;

theorem Th20: :: TOPREAL6:20
for a, r being real number st r > 0 holds
a in ].(a - r),(a + r).[
proof end;

theorem :: TOPREAL6:21
for a, r being real number st r >= 0 holds
a in [.(a - r),(a + r).]
proof end;

theorem Th22: :: TOPREAL6:22
for a, b being real number st a < b holds
( lower_bound ].a,b.[ = a & upper_bound ].a,b.[ = b )
proof end;

theorem :: TOPREAL6:23
canceled;

theorem Th24: :: TOPREAL6:24
for A being bounded Subset of REAL holds A c= [.(lower_bound A),(upper_bound A).]
proof end;

begin

registration
let T be TopStruct ;
let A be finite Subset of T;
cluster T | A -> finite ;
coherence
T | A is finite by PRE_TOPC:29;
end;

registration
let T be TopStruct ;
cluster empty -> connected Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is empty holds
b1 is connected
proof end;
end;

theorem Th25: :: TOPREAL6:25
for S, T being TopSpace st S,T are_homeomorphic & S is connected holds
T is connected
proof end;

theorem :: TOPREAL6:26
for T being TopSpace
for F being finite Subset-Family of T st ( for X being Subset of T st X in F holds
X is compact ) holds
union F is compact
proof end;

begin

theorem :: TOPREAL6:27
canceled;

theorem :: TOPREAL6:28
canceled;

theorem Th29: :: TOPREAL6:29
for A, B, C, D, a, b being set st A c= B & C c= D holds
product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D))
proof end;

theorem Th30: :: TOPREAL6:30
for A, B being Subset of REAL holds product ((1,2) --> (A,B)) is Subset of (TOP-REAL 2)
proof end;

theorem :: TOPREAL6:31
for a being Real holds
( |.|[0,a]|.| = abs a & |.|[a,0]|.| = abs a )
proof end;

theorem Th32: :: TOPREAL6:32
for p being Point of (Euclid 2)
for q being Point of (TOP-REAL 2) st p = 0. (TOP-REAL 2) & p = q holds
( q = <*0,0*> & q `1 = 0 & q `2 = 0 )
proof end;

theorem :: TOPREAL6:33
for p, q being Point of (Euclid 2)
for z being Point of (TOP-REAL 2) st p = 0.REAL 2 & q = z holds
dist (p,q) = |.z.|
proof end;

theorem Th34: :: TOPREAL6:34
for r being Real
for p being Point of (TOP-REAL 2) holds r * p = |[(r * (p `1)),(r * (p `2))]|
proof end;

theorem Th35: :: TOPREAL6:35
for r being Real
for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r holds
0 < r
proof end;

theorem Th36: :: TOPREAL6:36
for r being Real
for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> q & r <= 1 holds
r < 1
proof end;

theorem :: TOPREAL6:37
for s, p, q being Point of (TOP-REAL 2) st s in LSeg (p,q) & s <> p & s <> q & p `1 < q `1 holds
( p `1 < s `1 & s `1 < q `1 )
proof end;

theorem :: TOPREAL6:38
for s, p, q being Point of (TOP-REAL 2) st s in LSeg (p,q) & s <> p & s <> q & p `2 < q `2 holds
( p `2 < s `2 & s `2 < q `2 )
proof end;

theorem :: TOPREAL6:39
for D being non empty Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st
( q `1 < W-bound D & p <> q )
proof end;

theorem :: TOPREAL6:40
for D being non empty Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st
( q `1 > E-bound D & p <> q )
proof end;

theorem :: TOPREAL6:41
for D being non empty Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st
( q `2 > N-bound D & p <> q )
proof end;

theorem :: TOPREAL6:42
for D being non empty Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st
( q `2 < S-bound D & p <> q )
proof end;

registration
cluster non horizontal -> non empty Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st not b1 is horizontal holds
not b1 is empty
proof end;
cluster non vertical -> non empty Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st not b1 is vertical holds
not b1 is empty
proof end;
cluster being_Region -> open connected Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is being_Region holds
( b1 is open & b1 is connected ) by TOPREAL4:def 3;
cluster open connected -> being_Region Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is open & b1 is connected holds
b1 is being_Region by TOPREAL4:def 3;
end;

registration
cluster empty -> horizontal Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is empty holds
b1 is horizontal ;
cluster empty -> vertical Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is empty holds
b1 is vertical ;
end;

registration
cluster non empty convex Element of bool the carrier of (TOP-REAL 2);
existence
ex b1 being Subset of (TOP-REAL 2) st
( not b1 is empty & b1 is convex )
proof end;
end;

registration
let a, b be Point of (TOP-REAL 2);
cluster LSeg (a,b) -> connected ;
coherence
LSeg (a,b) is connected ;
end;

registration
cluster R^2-unit_square -> connected ;
coherence
R^2-unit_square is connected
proof end;
end;

registration
cluster being_simple_closed_curve -> connected Element of bool the carrier of (TOP-REAL 2);
coherence
for b1 being Subset of (TOP-REAL 2) st b1 is being_simple_closed_curve holds
b1 is connected
proof end;
end;

theorem :: TOPREAL6:43
for P being Subset of (TOP-REAL 2) holds LSeg ((NE-corner P),(SE-corner P)) c= L~ (SpStSeq P)
proof end;

theorem :: TOPREAL6:44
for P being Subset of (TOP-REAL 2) holds LSeg ((SW-corner P),(SE-corner P)) c= L~ (SpStSeq P)
proof end;

theorem :: TOPREAL6:45
for P being Subset of (TOP-REAL 2) holds LSeg ((SW-corner P),(NW-corner P)) c= L~ (SpStSeq P)
proof end;

theorem :: TOPREAL6:46
for C being Subset of (TOP-REAL 2) holds { p where p is Point of (TOP-REAL 2) : p `1 < W-bound C } is non empty connected convex Subset of (TOP-REAL 2)
proof end;

begin

theorem Th47: :: TOPREAL6:47
for q, p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for r being real number st e = q & p in Ball (e,r) holds
( (q `1) - r < p `1 & p `1 < (q `1) + r )
proof end;

theorem Th48: :: TOPREAL6:48
for q, p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for r being real number st e = q & p in Ball (e,r) holds
( (q `2) - r < p `2 & p `2 < (q `2) + r )
proof end;

theorem Th49: :: TOPREAL6:49
for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for r being real number st p = e holds
product ((1,2) --> (].((p `1) - (r / (sqrt 2))),((p `1) + (r / (sqrt 2))).[,].((p `2) - (r / (sqrt 2))),((p `2) + (r / (sqrt 2))).[)) c= Ball (e,r)
proof end;

theorem Th50: :: TOPREAL6:50
for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for r being real number st p = e holds
Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))
proof end;

theorem Th51: :: TOPREAL6:51
for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for P being Subset of (TOP-REAL 2)
for r being real number st P = Ball (e,r) & p = e holds
proj1 .: P = ].((p `1) - r),((p `1) + r).[
proof end;

theorem Th52: :: TOPREAL6:52
for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for P being Subset of (TOP-REAL 2)
for r being real number st P = Ball (e,r) & p = e holds
proj2 .: P = ].((p `2) - r),((p `2) + r).[
proof end;

theorem :: TOPREAL6:53
for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for D being non empty Subset of (TOP-REAL 2)
for r being real number st D = Ball (e,r) & p = e holds
W-bound D = (p `1) - r
proof end;

theorem :: TOPREAL6:54
for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for D being non empty Subset of (TOP-REAL 2)
for r being real number st D = Ball (e,r) & p = e holds
E-bound D = (p `1) + r
proof end;

theorem :: TOPREAL6:55
for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for D being non empty Subset of (TOP-REAL 2)
for r being real number st D = Ball (e,r) & p = e holds
S-bound D = (p `2) - r
proof end;

theorem :: TOPREAL6:56
for p being Point of (TOP-REAL 2)
for e being Point of (Euclid 2)
for D being non empty Subset of (TOP-REAL 2)
for r being real number st D = Ball (e,r) & p = e holds
N-bound D = (p `2) + r
proof end;

theorem :: TOPREAL6:57
for e being Point of (Euclid 2)
for D being non empty Subset of (TOP-REAL 2)
for r being real number st D = Ball (e,r) holds
not D is horizontal
proof end;

theorem :: TOPREAL6:58
for e being Point of (Euclid 2)
for D being non empty Subset of (TOP-REAL 2)
for r being real number st D = Ball (e,r) holds
not D is vertical
proof end;

theorem :: TOPREAL6:59
for a being Real
for f being Point of (Euclid 2)
for x being Point of (TOP-REAL 2) st x in Ball (f,a) holds
not |[((x `1) - (2 * a)),(x `2)]| in Ball (f,a)
proof end;

theorem :: TOPREAL6:60
for a being Real
for X being non empty compact Subset of (TOP-REAL 2)
for p being Point of (Euclid 2) st p = 0. (TOP-REAL 2) & a > 0 holds
X c= Ball (p,(((((abs (E-bound X)) + (abs (N-bound X))) + (abs (W-bound X))) + (abs (S-bound X))) + a))
proof end;

theorem Th61: :: TOPREAL6:61
for r being real number
for M being non empty Reflexive symmetric triangle MetrStruct
for z being Point of M st r < 0 holds
Sphere (z,r) = {}
proof end;

theorem :: TOPREAL6:62
for M being non empty Reflexive discerning MetrStruct
for z being Point of M holds Sphere (z,0) = {z}
proof end;

theorem :: TOPREAL6:63
for r being real number
for M being non empty Reflexive symmetric triangle MetrStruct
for z being Point of M st r < 0 holds
cl_Ball (z,r) = {}
proof end;

theorem :: TOPREAL6:64
for M being non empty MetrSpace
for z being Point of M holds cl_Ball (z,0) = {z}
proof end;

Lm1: for M being non empty MetrSpace
for z being Point of M
for r being real number
for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds
A ` is open
proof end;

theorem Th65: :: TOPREAL6:65
for M being non empty MetrSpace
for z being Point of M
for r being real number
for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds
A is closed
proof end;

theorem :: TOPREAL6:66
for n being Element of NAT
for w being Point of (Euclid n)
for A being Subset of (TOP-REAL n)
for r being real number st A = cl_Ball (w,r) holds
A is closed
proof end;

theorem Th67: :: TOPREAL6:67
for r being real number
for M being non empty Reflexive symmetric triangle MetrStruct
for x being Element of M holds cl_Ball (x,r) is bounded
proof end;

theorem Th68: :: TOPREAL6:68
for M being non empty MetrSpace
for z being Point of M
for r being real number
for A being Subset of (TopSpaceMetr M) st A = Sphere (z,r) holds
A is closed
proof end;

theorem :: TOPREAL6:69
for n being Element of NAT
for w being Point of (Euclid n)
for A being Subset of (TOP-REAL n)
for r being real number st A = Sphere (w,r) holds
A is closed
proof end;

theorem :: TOPREAL6:70
for M being non empty MetrSpace
for z being Point of M
for r being real number holds Sphere (z,r) is bounded
proof end;

theorem Th71: :: TOPREAL6:71
for n being Element of NAT
for A being Subset of (TOP-REAL n) st A is Bounded holds
Cl A is Bounded
proof end;

theorem :: TOPREAL6:72
for M being non empty MetrStruct holds
( M is bounded iff for X being Subset of M holds X is bounded )
proof end;

theorem Th73: :: TOPREAL6:73
for M being non empty Reflexive symmetric triangle MetrStruct
for X, Y being Subset of M st the carrier of M = X \/ Y & not M is bounded & X is bounded holds
not Y is bounded
proof end;

theorem :: TOPREAL6:74
for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st n >= 1 & the carrier of (TOP-REAL n) = X \/ Y & X is Bounded holds
not Y is Bounded
proof end;

theorem :: TOPREAL6:75
canceled;

theorem Th76: :: TOPREAL6:76
for n being Element of NAT
for A, B being Subset of (TOP-REAL n) st A is Bounded & B is Bounded holds
A \/ B is Bounded
proof end;

begin

registration
let X be non empty Subset of REAL;
cluster Cl X -> non empty ;
coherence
not Cl X is empty by MEASURE6:94, XBOOLE_1:3;
end;

registration
let D be bounded_below Subset of REAL;
cluster Cl D -> bounded_below ;
coherence
Cl D is bounded_below
proof end;
end;

registration
let D be bounded_above Subset of REAL;
cluster Cl D -> bounded_above ;
coherence
Cl D is bounded_above
proof end;
end;

theorem Th77: :: TOPREAL6:77
for D being non empty bounded_below Subset of REAL holds lower_bound D = lower_bound (Cl D)
proof end;

theorem Th78: :: TOPREAL6:78
for D being non empty bounded_above Subset of REAL holds upper_bound D = upper_bound (Cl D)
proof end;

registration
cluster R^1 -> T_2 ;
coherence
R^1 is T_2 by PCOMPS_1:38, TOPMETR:def 7;
end;

Lm2: R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)
by PCOMPS_1:def 6, TOPMETR:def 7;

theorem Th79: :: TOPREAL6:79
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is closed iff B is closed )
proof end;

theorem :: TOPREAL6:80
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
Cl A = Cl B
proof end;

theorem Th81: :: TOPREAL6:81
for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is compact iff B is compact )
proof end;

registration
cluster finite -> compact Element of bool REAL;
coherence
for b1 being Subset of REAL st b1 is finite holds
b1 is compact by Th81, TOPMETR:24;
end;

registration
let a, b be real number ;
cluster K217(a,b) -> compact Subset of REAL;
coherence
for b1 being Subset of REAL st b1 = [.a,b.] holds
b1 is compact by RCOMP_1:24;
end;

theorem :: TOPREAL6:82
for a, b being real number holds
( a <> b iff Cl ].a,b.[ = [.a,b.] )
proof end;

registration
cluster non empty finite V195() V196() V197() bounded Element of bool REAL;
existence
ex b1 being Subset of REAL st
( not b1 is empty & b1 is finite & b1 is bounded )
proof end;
end;

theorem Th83: :: TOPREAL6:83
for T being TopStruct
for f being RealMap of T
for g being Function of T,R^1 st f = g holds
( f is continuous iff g is continuous )
proof end;

theorem Th84: :: TOPREAL6:84
for A, B being Subset of REAL
for f being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being Real holds f . [x,y] = <*x,y*> ) holds
f .: [:A,B:] = product ((1,2) --> (A,B))
proof end;

theorem Th85: :: TOPREAL6:85
for f being Function of [:R^1,R^1:],(TOP-REAL 2) st ( for x, y being Real holds f . [x,y] = <*x,y*> ) holds
f is being_homeomorphism
proof end;

theorem :: TOPREAL6:86
[:R^1,R^1:], TOP-REAL 2 are_homeomorphic
proof end;

begin

theorem Th87: :: TOPREAL6:87
for A, B being compact Subset of REAL holds product ((1,2) --> (A,B)) is compact Subset of (TOP-REAL 2)
proof end;

theorem Th88: :: TOPREAL6:88
for P being Subset of (TOP-REAL 2) st P is Bounded & P is closed holds
P is compact
proof end;

theorem Th89: :: TOPREAL6:89
for P being Subset of (TOP-REAL 2) st P is Bounded holds
for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P)
proof end;

theorem Th90: :: TOPREAL6:90
for P being Subset of (TOP-REAL 2) holds proj1 .: (Cl P) c= Cl (proj1 .: P)
proof end;

theorem Th91: :: TOPREAL6:91
for P being Subset of (TOP-REAL 2) holds proj2 .: (Cl P) c= Cl (proj2 .: P)
proof end;

theorem Th92: :: TOPREAL6:92
for P being Subset of (TOP-REAL 2) st P is Bounded holds
Cl (proj1 .: P) = proj1 .: (Cl P)
proof end;

theorem Th93: :: TOPREAL6:93
for P being Subset of (TOP-REAL 2) st P is Bounded holds
Cl (proj2 .: P) = proj2 .: (Cl P)
proof end;

theorem :: TOPREAL6:94
for D being non empty Subset of (TOP-REAL 2) st D is Bounded holds
W-bound D = W-bound (Cl D)
proof end;

theorem :: TOPREAL6:95
for D being non empty Subset of (TOP-REAL 2) st D is Bounded holds
E-bound D = E-bound (Cl D)
proof end;

theorem :: TOPREAL6:96
for D being non empty Subset of (TOP-REAL 2) st D is Bounded holds
N-bound D = N-bound (Cl D)
proof end;

theorem :: TOPREAL6:97
for D being non empty Subset of (TOP-REAL 2) st D is Bounded holds
S-bound D = S-bound (Cl D)
proof end;

theorem Th98: :: TOPREAL6:98
for n being Element of NAT
for A, B being Subset of (TOP-REAL n) st ( A is Bounded or B is Bounded ) holds
A /\ B is Bounded
proof end;

theorem :: TOPREAL6:99
for n being Element of NAT
for A, B being Subset of (TOP-REAL n) st not A is Bounded & B is Bounded holds
not A \ B is Bounded
proof end;

begin

definition
let n be Element of NAT ;
let a, b be Point of (TOP-REAL n);
func dist (a,b) -> Real means :Def1: :: TOPREAL6:def 1
 ex p, q being Point of (Euclid n) st
( p = a & q = b & it = dist (p,q) );
existence
ex b1 being Real ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist (p,q) )
proof end;
uniqueness
for b1, b2 being Real st ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist (p,q) ) & ex p, q being Point of (Euclid n) st
( p = a & q = b & b2 = dist (p,q) ) holds
b1 = b2 ;
commutativity
for b1 being Real
for a, b being Point of (TOP-REAL n) st ex p, q being Point of (Euclid n) st
( p = a & q = b & b1 = dist (p,q) ) holds
ex p, q being Point of (Euclid n) st
( p = b & q = a & b1 = dist (p,q) ) ;
end;

:: deftheorem Def1 defines dist TOPREAL6:def 1 :
for n being Element of NAT
for a, b being Point of (TOP-REAL n)
for b4 being Real holds
( b4 = dist (a,b) iff ex p, q being Point of (Euclid n) st
( p = a & q = b & b4 = dist (p,q) ) );

theorem Th100: :: TOPREAL6:100
for r1, s1, r2, s2 being real number
for u, v being Point of (Euclid 2) st u = |[r1,s1]| & v = |[r2,s2]| holds
dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2))
proof end;

theorem Th101: :: TOPREAL6:101
for p, q being Point of (TOP-REAL 2) holds dist (p,q) = sqrt ((((p `1) - (q `1)) ^2) + (((p `2) - (q `2)) ^2))
proof end;

theorem :: TOPREAL6:102
for n being Element of NAT
for p being Point of (TOP-REAL n) holds dist (p,p) = 0
proof end;

theorem :: TOPREAL6:103
for n being Element of NAT
for p, q, r being Point of (TOP-REAL n) holds dist (p,r) <= (dist (p,q)) + (dist (q,r))
proof end;

theorem :: TOPREAL6:104
for x1, x2, y1, y2 being real number
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)
proof end;