:: Intersections of Intervals and Balls in TOP-REAL n
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received May 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

theorem :: TOPREAL9:1
canceled;

theorem Th2: :: TOPREAL9:2
for n being Element of NAT
for x, y, z being Point of (TOP-REAL n) st x + y = x + z holds
y = z
proofend;

theorem Th3: :: TOPREAL9:3
for n being Element of NAT
for x being Point of (TOP-REAL n) st not n is empty holds
x <> x + (1.REAL n)
proofend;

theorem Th4: :: TOPREAL9:4
for n being Element of NAT
for r being real number
for y, z being Point of (TOP-REAL n)
for x being set st x = ((1 - r) * y) + (r * z) holds
( ( not x = y or r = 0 or y = z ) &amp; ( ( r = 0 or y = z ) implies x = y ) &amp; ( not x = z or r = 1 or y = z ) &amp; ( ( r = 1 or y = z ) implies x = z ) )
proofend;

theorem Th5: :: TOPREAL9:5
for f being real-valued FinSequence holds |.f.| ^2 = Sum (sqr f)
proofend;

theorem Th6: :: TOPREAL9:6
for r being real number
for M being non empty MetrSpace
for z1, z2, z3 being Point of M st z1 <> z2 &amp; z1 in cl_Ball (z3,r) &amp; z2 in cl_Ball (z3,r) holds
r > 0
proofend;

begin

definition
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real number ;
func Ball (x,r) ->  Subset of (TOP-REAL n) equals :: TOPREAL9:def 1
 {  p where p is Point of (TOP-REAL n) : |.(p - x).| < r  }  ;
coherence
  {  p where p is Point of (TOP-REAL n) : |.(p - x).| < r  }  is Subset of (TOP-REAL n)
proofend;
func cl_Ball (x,r) ->  Subset of (TOP-REAL n) equals :: TOPREAL9:def 2
 {  p where p is Point of (TOP-REAL n) : |.(p - x).| <= r  }  ;
coherence
  {  p where p is Point of (TOP-REAL n) : |.(p - x).| <= r  }  is Subset of (TOP-REAL n)
proofend;
func Sphere (x,r) ->  Subset of (TOP-REAL n) equals :: TOPREAL9:def 3
 {  p where p is Point of (TOP-REAL n) : |.(p - x).| = r  }  ;
coherence
  {  p where p is Point of (TOP-REAL n) : |.(p - x).| = r  }  is Subset of (TOP-REAL n)
proofend;
end;

:: deftheorem  defines Ball TOPREAL9:def_1_:_
 for n being Nat
for x being Point of (TOP-REAL n)
for r being real number holds Ball (x,r) =  {  p where p is Point of (TOP-REAL n) : |.(p - x).| < r  }  ;

:: deftheorem  defines cl_Ball TOPREAL9:def_2_:_
 for n being Nat
for x being Point of (TOP-REAL n)
for r being real number holds cl_Ball (x,r) =  {  p where p is Point of (TOP-REAL n) : |.(p - x).| <= r  }  ;

:: deftheorem  defines Sphere TOPREAL9:def_3_:_
 for n being Nat
for x being Point of (TOP-REAL n)
for r being real number holds Sphere (x,r) =  {  p where p is Point of (TOP-REAL n) : |.(p - x).| = r  }  ;

theorem Th7: :: TOPREAL9:7
for n being Element of NAT
for r being real number
for y, x being Point of (TOP-REAL n) holds
( y in Ball (x,r) iff |.(y - x).| < r )
proofend;

theorem Th8: :: TOPREAL9:8
for n being Element of NAT
for r being real number
for y, x being Point of (TOP-REAL n) holds
( y in cl_Ball (x,r) iff |.(y - x).| <= r )
proofend;

theorem Th9: :: TOPREAL9:9
for n being Element of NAT
for r being real number
for y, x being Point of (TOP-REAL n) holds
( y in Sphere (x,r) iff |.(y - x).| = r )
proofend;

theorem :: TOPREAL9:10
for n being Element of NAT
for r being real number
for y being Point of (TOP-REAL n) st y in Ball ((0. (TOP-REAL n)),r) holds
|.y.| < r
proofend;

theorem :: TOPREAL9:11
for n being Element of NAT
for r being real number
for y being Point of (TOP-REAL n) st y in cl_Ball ((0. (TOP-REAL n)),r) holds
|.y.| <= r
proofend;

theorem :: TOPREAL9:12
for n being Element of NAT
for r being real number
for y being Point of (TOP-REAL n) st y in Sphere ((0. (TOP-REAL n)),r) holds
|.y.| = r
proofend;

theorem Th13: :: TOPREAL9:13
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n)
for e being Point of (Euclid n) st x = e holds
Ball (e,r) = Ball (x,r)
proofend;

theorem Th14: :: TOPREAL9:14
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n)
for e being Point of (Euclid n) st x = e holds
cl_Ball (e,r) = cl_Ball (x,r)
proofend;

theorem Th15: :: TOPREAL9:15
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n)
for e being Point of (Euclid n) st x = e holds
Sphere (e,r) = Sphere (x,r)
proofend;

theorem :: TOPREAL9:16
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) holds Ball (x,r) c= cl_Ball (x,r)
proofend;

theorem Th17: :: TOPREAL9:17
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) holds Sphere (x,r) c= cl_Ball (x,r)
proofend;

theorem Th18: :: TOPREAL9:18
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) holds (Ball (x,r)) \/ (Sphere (x,r)) = cl_Ball (x,r)
proofend;

theorem Th19: :: TOPREAL9:19
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) holds Ball (x,r) misses Sphere (x,r)
proofend;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real non positive number ;
cluster Ball (x,r) ->  empty ;
coherence
 Ball (x,r) is empty
proofend;
end;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real positive number ;
cluster Ball (x,r) ->  non empty ;
coherence
 not Ball (x,r) is empty
proofend;
end;

theorem :: TOPREAL9:20
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) st not Ball (x,r) is empty holds
r > 0 ;

theorem :: TOPREAL9:21
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) st Ball (x,r) is empty holds
r <= 0 ;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real negative number ;
cluster cl_Ball (x,r) ->  empty ;
coherence
 cl_Ball (x,r) is empty
proofend;
end;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real non negative number ;
cluster cl_Ball (x,r) ->  non empty ;
coherence
 not cl_Ball (x,r) is empty
proofend;
end;

theorem :: TOPREAL9:22
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) st not cl_Ball (x,r) is empty holds
r >= 0 ;

theorem :: TOPREAL9:23
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) st cl_Ball (x,r) is empty holds
r < 0 ;

theorem Th24: :: TOPREAL9:24
for n being Element of NAT
for a, b, r being real number
for x, z, y being Point of (TOP-REAL n) st a + b = 1 &amp; (abs a) + (abs b) = 1 &amp; b <> 0 &amp; x in cl_Ball (z,r) &amp; y in Ball (z,r) holds
(a * x) + (b * y) in Ball (z,r)
proofend;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real number ;
cluster Ball (x,r) ->  open ;
coherence
 Ball (x,r) is open
proofend;
cluster cl_Ball (x,r) ->  closed ;
coherence
 cl_Ball (x,r) is closed
proofend;
cluster Sphere (x,r) ->  closed ;
coherence
 Sphere (x,r) is closed
proofend;
end;

registration
let n be Element of NAT ;
let x be Point of (TOP-REAL n);
let r be real number ;
cluster Ball (x,r) ->  bounded ;
coherence
 Ball (x,r) is bounded
proofend;
cluster cl_Ball (x,r) ->  bounded ;
coherence
 cl_Ball (x,r) is bounded
proofend;
cluster Sphere (x,r) ->  bounded ;
coherence
 Sphere (x,r) is bounded
proofend;
end;

Lm1:  for n being Element of NAT
for a being real number
for P being Subset of (TOP-REAL n)
for Q being Point of (TOP-REAL n) st P =  {  q where q is Point of (TOP-REAL n) : |.(q - Q).| <= a  }  holds
P is convex
proofend;

Lm2:  for n being Element of NAT
for a being real number
for P being Subset of (TOP-REAL n)
for Q being Point of (TOP-REAL n) st P =  {  q where q is Point of (TOP-REAL n) : |.(q - Q).| < a  }  holds
P is convex
proofend;

:: Convex subsets of TOP-REAL n
registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real number ;
cluster Ball (x,r) ->  convex ;
coherence
 Ball (x,r) is convex
proofend;
cluster cl_Ball (x,r) ->  convex ;
coherence
 cl_Ball (x,r) is convex
proofend;
end;

definition
let n be Nat;
let f be Function of (TOP-REAL n),(TOP-REAL n);
attrf is homogeneous  means :Def4: :: TOPREAL9:def 4
 for r being real number
for x being Point of (TOP-REAL n) holds f . (r * x) = r * (f . x);
end;

:: deftheorem Def4 defines homogeneous TOPREAL9:def_4_:_
 for n being Nat
for f being Function of (TOP-REAL n),(TOP-REAL n) holds
( f is homogeneous iff for r being real number
for x being Point of (TOP-REAL n) holds f . (r * x) = r * (f . x) );

registration
let n be Element of NAT ;
cluster(TOP-REAL n) --> (0. (TOP-REAL n)) ->  additive homogeneous ;
coherence
 ( (TOP-REAL n) --> (0. (TOP-REAL n)) is homogeneous &amp; (TOP-REAL n) --> (0. (TOP-REAL n)) is additive )
proofend;
end;

registration
let n be Element of NAT ;
clusterV16() V21() V30( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) continuous additive homogeneous for Element of K6(K7( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)));
existence
 ex b1 being Function of (TOP-REAL n),(TOP-REAL n) st
( b1 is homogeneous &amp; b1 is additive &amp; b1 is continuous )
proofend;
end;

registration
let a, c be real number ;
cluster AffineMap (a,0,c,0) ->  additive homogeneous ;
coherence
 ( AffineMap (a,0,c,0) is homogeneous &amp; AffineMap (a,0,c,0) is additive )
proofend;
end;

theorem :: TOPREAL9:25
for n being Element of NAT
for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n)
for X being convex Subset of (TOP-REAL n) holds f .: X is convex
proofend;

definition
let n be Nat;
let p, q be Point of (TOP-REAL n);
func halfline (p,q) ->  Subset of (TOP-REAL n) equals :: TOPREAL9:def 5
 {  (((1 - l) * p) + (l * q)) where l is Real : 0 <= l  }  ;
coherence
  {  (((1 - l) * p) + (l * q)) where l is Real : 0 <= l  }  is Subset of (TOP-REAL n)
proofend;
end;

:: deftheorem  defines halfline TOPREAL9:def_5_:_
 for n being Nat
for p, q being Point of (TOP-REAL n) holds halfline (p,q) =  {  (((1 - l) * p) + (l * q)) where l is Real : 0 <= l  }  ;

theorem Th26: :: TOPREAL9:26
for n being Element of NAT
for p, q being Point of (TOP-REAL n)
for x being set holds
( x in halfline (p,q) iff ex l being real number st
( x = ((1 - l) * p) + (l * q) &amp; 0 <= l ) )
proofend;

registration
let n be Element of NAT ;
let p, q be Point of (TOP-REAL n);
cluster halfline (p,q) ->  non empty ;
coherence
 not halfline (p,q) is empty
proofend;
end;

theorem Th27: :: TOPREAL9:27
for n being Element of NAT
for p, q being Point of (TOP-REAL n) holds p in halfline (p,q)
proofend;

theorem Th28: :: TOPREAL9:28
for n being Element of NAT
for q, p being Point of (TOP-REAL n) holds q in halfline (p,q)
proofend;

theorem Th29: :: TOPREAL9:29
for n being Element of NAT
for p being Point of (TOP-REAL n) holds halfline (p,p) = {p}
proofend;

theorem Th30: :: TOPREAL9:30
for n being Element of NAT
for x, p, q being Point of (TOP-REAL n) st x in halfline (p,q) holds
halfline (p,x) c= halfline (p,q)
proofend;

theorem :: TOPREAL9:31
for n being Element of NAT
for x, p, q being Point of (TOP-REAL n) st x in halfline (p,q) &amp; x <> p holds
halfline (p,q) = halfline (p,x)
proofend;

theorem :: TOPREAL9:32
for n being Element of NAT
for p, q being Point of (TOP-REAL n) holds LSeg (p,q) c= halfline (p,q)
proofend;

registration
let n be Element of NAT ;
let p, q be Point of (TOP-REAL n);
cluster halfline (p,q) ->  convex ;
coherence
 halfline (p,q) is convex
proofend;
end;

theorem Th33: :: TOPREAL9:33
for n being Element of NAT
for r being real number
for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) &amp; z in Ball (x,r) holds
(LSeg (y,z)) /\ (Sphere (x,r)) = {y}
proofend;

theorem Th34: :: TOPREAL9:34
for n being Element of NAT
for r being real number
for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) &amp; z in Sphere (x,r) holds
(LSeg (y,z)) \ {y,z} c= Ball (x,r)
proofend;

theorem Th35: :: TOPREAL9:35
for n being Element of NAT
for r being real number
for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) &amp; z in Sphere (x,r) holds
(LSeg (y,z)) /\ (Sphere (x,r)) = {y,z}
proofend;

theorem Th36: :: TOPREAL9:36
for n being Element of NAT
for r being real number
for y, x, z being Point of (TOP-REAL n) st y in Sphere (x,r) &amp; z in Sphere (x,r) holds
(halfline (y,z)) /\ (Sphere (x,r)) = {y,z}
proofend;

theorem Th37: :: TOPREAL9:37
for n being Element of NAT
for r, a being real number
for y, z, x being Point of (TOP-REAL n)
for S, T, X being Element of REAL n st S = y &amp; T = z &amp; X = x &amp; y <> z &amp; y in Ball (x,r) &amp; a = ((- (2 * |((z - y),(y - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - y),(y - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) holds
ex e being Point of (TOP-REAL n) st
( {e} = (halfline (y,z)) /\ (Sphere (x,r)) &amp; e = ((1 - a) * y) + (a * z) )
proofend;

theorem Th38: :: TOPREAL9:38
for n being Element of NAT
for r, a being real number
for y, z, x being Point of (TOP-REAL n)
for S, T, Y being Element of REAL n st S = ((1 / 2) * y) + ((1 / 2) * z) &amp; T = z &amp; Y = x &amp; y <> z &amp; y in Sphere (x,r) &amp; z in cl_Ball (x,r) holds
ex e being Point of (TOP-REAL n) st
( e <> y &amp; {y,e} = (halfline (y,z)) /\ (Sphere (x,r)) &amp; ( z in Sphere (x,r) implies e = z ) &amp; ( not z in Sphere (x,r) &amp; a = ((- (2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((z - (((1 / 2) * y) + ((1 / 2) * z))),((((1 / 2) * y) + ((1 / 2) * z)) - x))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - a) * (((1 / 2) * y) + ((1 / 2) * z))) + (a * z) ) )
proofend;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real negative number ;
cluster Sphere (x,r) ->  empty ;
coherence
 Sphere (x,r) is empty
proofend;
end;

registration
let n be non empty Nat;
let x be Point of (TOP-REAL n);
let r be real non negative number ;
cluster Sphere (x,r) ->  non empty ;
coherence
 not Sphere (x,r) is empty
proofend;
end;

theorem :: TOPREAL9:39
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) st not Sphere (x,r) is empty holds
r >= 0 ;

theorem :: TOPREAL9:40
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) st not n is empty &amp; Sphere (x,r) is empty holds
r < 0 ;

begin

theorem :: TOPREAL9:41
for a, b being real number
for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `1 = (a * (s `1)) + (b * (t `1))
proofend;

theorem :: TOPREAL9:42
for a, b being real number
for s, t being Point of (TOP-REAL 2) holds ((a * s) + (b * t)) `2 = (a * (s `2)) + (b * (t `2))
proofend;

theorem Th43: :: TOPREAL9:43
for a, b, r being real number
for t being Point of (TOP-REAL 2) holds
( t in circle (a,b,r) iff |.(t - |[a,b]|).| = r )
proofend;

theorem Th44: :: TOPREAL9:44
for a, b, r being real number
for t being Point of (TOP-REAL 2) holds
( t in closed_inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| <= r )
proofend;

theorem Th45: :: TOPREAL9:45
for a, b, r being real number
for t being Point of (TOP-REAL 2) holds
( t in inside_of_circle (a,b,r) iff |.(t - |[a,b]|).| < r )
proofend;

registration
let a, b be real number ;
let r be real positive number ;
cluster inside_of_circle (a,b,r) ->  non empty ;
coherence
 not inside_of_circle (a,b,r) is empty
proofend;
end;

registration
let a, b be real number ;
let r be real non negative number ;
cluster closed_inside_of_circle (a,b,r) ->  non empty ;
coherence
 not closed_inside_of_circle (a,b,r) is empty
proofend;
end;

theorem :: TOPREAL9:46
for a, b, r being real number holds circle (a,b,r) c= closed_inside_of_circle (a,b,r)
proofend;

theorem Th47: :: TOPREAL9:47
for a, b, r being real number
for x being Point of (Euclid 2) st x = |[a,b]| holds
cl_Ball (x,r) = closed_inside_of_circle (a,b,r)
proofend;

theorem Th48: :: TOPREAL9:48
for a, b, r being real number
for x being Point of (Euclid 2) st x = |[a,b]| holds
Ball (x,r) = inside_of_circle (a,b,r)
proofend;

theorem Th49: :: TOPREAL9:49
for a, b, r being real number
for x being Point of (Euclid 2) st x = |[a,b]| holds
Sphere (x,r) = circle (a,b,r)
proofend;

theorem Th50: :: TOPREAL9:50
for a, b, r being real number holds Ball (|[a,b]|,r) = inside_of_circle (a,b,r)
proofend;

theorem :: TOPREAL9:51
for a, b, r being real number holds cl_Ball (|[a,b]|,r) = closed_inside_of_circle (a,b,r)
proofend;

theorem Th52: :: TOPREAL9:52
for a, b, r being real number holds Sphere (|[a,b]|,r) = circle (a,b,r)
proofend;

theorem :: TOPREAL9:53
for a, b, r being real number holds inside_of_circle (a,b,r) c= closed_inside_of_circle (a,b,r)
proofend;

theorem :: TOPREAL9:54
for a, b, r being real number holds inside_of_circle (a,b,r) misses circle (a,b,r)
proofend;

theorem :: TOPREAL9:55
for a, b, r being real number holds (inside_of_circle (a,b,r)) \/ (circle (a,b,r)) = closed_inside_of_circle (a,b,r)
proofend;

theorem :: TOPREAL9:56
for r being real number
for s being Point of (TOP-REAL 2) st s in Sphere ((0. (TOP-REAL 2)),r) holds
((s `1) ^2) + ((s `2) ^2) = r ^2
proofend;

theorem :: TOPREAL9:57
for a, b, r being real number
for s, t being Point of (TOP-REAL 2) st s <> t &amp; s in closed_inside_of_circle (a,b,r) &amp; t in closed_inside_of_circle (a,b,r) holds
r > 0
proofend;

theorem :: TOPREAL9:58
for a, b, w, r being real number
for s, t being Point of (TOP-REAL 2)
for S, T, X being Element of REAL 2 st S = s &amp; T = t &amp; X = |[a,b]| &amp; w = ((- (2 * |((t - s),(s - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - |[a,b]|))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) &amp; s <> t &amp; s in inside_of_circle (a,b,r) holds
ex e being Point of (TOP-REAL 2) st
( {e} = (halfline (s,t)) /\ (circle (a,b,r)) &amp; e = ((1 - w) * s) + (w * t) )
proofend;

theorem :: TOPREAL9:59
for a, b, r being real number
for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) &amp; t in inside_of_circle (a,b,r) holds
(LSeg (s,t)) /\ (circle (a,b,r)) = {s}
proofend;

theorem :: TOPREAL9:60
for a, b, r being real number
for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) &amp; t in circle (a,b,r) holds
(LSeg (s,t)) \ {s,t} c= inside_of_circle (a,b,r)
proofend;

theorem :: TOPREAL9:61
for a, b, r being real number
for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) &amp; t in circle (a,b,r) holds
(LSeg (s,t)) /\ (circle (a,b,r)) = {s,t}
proofend;

theorem :: TOPREAL9:62
for a, b, r being real number
for s, t being Point of (TOP-REAL 2) st s in circle (a,b,r) &amp; t in circle (a,b,r) holds
(halfline (s,t)) /\ (circle (a,b,r)) = {s,t}
proofend;

theorem :: TOPREAL9:63
for a, b, r, w being real number
for s, t being Point of (TOP-REAL 2)
for S, T, Y being Element of REAL 2 st S = ((1 / 2) * s) + ((1 / 2) * t) &amp; T = t &amp; Y = |[a,b]| &amp; s <> t &amp; s in circle (a,b,r) &amp; t in closed_inside_of_circle (a,b,r) holds
ex e being Point of (TOP-REAL 2) st
( e <> s &amp; {s,e} = (halfline (s,t)) /\ (circle (a,b,r)) &amp; ( t in Sphere (|[a,b]|,r) implies e = t ) &amp; ( not t in Sphere (|[a,b]|,r) &amp; w = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - |[a,b]|))|),((Sum (sqr (S - Y))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e = ((1 - w) * (((1 / 2) * s) + ((1 / 2) * t))) + (w * t) ) )
proofend;

registration
let a, b, r be real number ;
cluster inside_of_circle (a,b,r) ->  convex ;
coherence
 inside_of_circle (a,b,r) is convex
proofend;
cluster closed_inside_of_circle (a,b,r) ->  convex ;
coherence
 closed_inside_of_circle (a,b,r) is convex
proofend;
end;