:: On the Geometry of a Go-board
::  by Andrzej Trybulec
::
:: Received July 9, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, REAL_1, PRE_TOPC, EUCLID, GOBOARD1, ARYTM_3,
      MCART_1, ARYTM_1, RELAT_1, XBOOLE_0, METRIC_1, XXREAL_0, CARD_1,
      PCOMPS_1, RCOMP_1, STRUCT_0, CONNSP_2, TOPS_1, TARSKI, SQUARE_1, FUNCT_1,
      FINSEQ_1, TREES_1, GOBOARD5, COMPLEX1, RLTOPSP1, SUPINF_2, NAT_1;
 notations TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0,
      XCMPLX_0, COMPLEX1, REAL_1, NAT_1, SQUARE_1, NAT_D, BINOP_1, FINSEQ_1,
      MATRIX_0, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, CONNSP_2, PCOMPS_1,
      RLVECT_1, RLTOPSP1, EUCLID, GOBOARD1, GOBOARD5;
 constructors REAL_1, SQUARE_1, NAT_1, COMPLEX1, NAT_D, TOPS_1, CONNSP_2,
      PCOMPS_1, GOBOARD1, GOBOARD5, FUNCSDOM, BINOP_2;
 registrations RELSET_1, XXREAL_0, XREAL_0, STRUCT_0, METRIC_1, PCOMPS_1,
      EUCLID, TOPS_1, PRE_TOPC, SQUARE_1, ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, ARITHM;


begin

reserve n for Nat,
  i,j for Nat,
  r,s,r1,s1,r2,s2,r9,s9 for Real,
  p,q for Point of TOP-REAL 2,
  G for Go-board,
  x,y for set,
  v for Point of Euclid 2;

theorem :: GOBOARD6:1
  for M being non empty Reflexive MetrStruct, u being Point of M, r
  being Real holds r > 0 implies u in Ball(u,r);

theorem :: GOBOARD6:2
  for p being Point of Euclid n, q being Point of TOP-REAL n, r
  being Real st p = q & r > 0 holds Ball (p, r) is a_neighborhood of q;

theorem :: GOBOARD6:3
  for B being Subset of TOP-REAL n, u being Point of Euclid n st B
  = Ball(u,r) holds B is open;

theorem :: GOBOARD6:4
  for M being non empty MetrSpace, u being Point of M, P being
Subset of TopSpaceMetr(M) holds u in Int P iff ex r being Real st r > 0
  & Ball(u,r) c= P;

theorem :: GOBOARD6:5
  for u being Point of Euclid n, P being Subset of TOP-REAL n holds
  u in Int P iff ex r being Real st r > 0 & Ball(u,r) c= P;

theorem :: GOBOARD6:6  :: TOPREAL3:12
  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);

theorem :: GOBOARD6:7
  for u being Point of Euclid 2 st u = |[r,s]| holds 0 <= r2 & r2
  < r1 implies |[r+r2,s]| in Ball(u,r1);

theorem :: GOBOARD6:8
  for u being Point of Euclid 2 st u = |[r,s]| holds 0 <= s2 & s2
  < s1 implies |[r,s+s2]| in Ball(u,s1);

theorem :: GOBOARD6:9
  for u being Point of Euclid 2 st u = |[r,s]| holds 0 <= r2 & r2
  < r1 implies |[r-r2,s]| in Ball(u,r1);

theorem :: GOBOARD6:10
  for u being Point of Euclid 2 st u = |[r,s]| holds 0 <= s2 & s2
  < s1 implies |[r,s-s2]| in Ball(u,s1);

theorem :: GOBOARD6:11
  1 <= i & i < len G & 1 <= j & j < width G implies G*(i,j)+G*(i+1
  ,j+1) = G*(i,j+1)+G*(i+1,j);

theorem :: GOBOARD6:12
  Int v_strip(G,0) = { |[r,s]| : r < G*(1,1)`1 };

theorem :: GOBOARD6:13
  Int v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 < r };

theorem :: GOBOARD6:14
  1 <= i & i < len G implies Int v_strip(G,i) = { |[r,s]| : G*(i,1
  )`1 < r & r < G*(i+1,1)`1 };

theorem :: GOBOARD6:15
  Int h_strip(G,0) = { |[r,s]| : s < G*(1,1)`2 };

theorem :: GOBOARD6:16
  Int h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 < s };

theorem :: GOBOARD6:17
  1 <= j & j < width G implies Int h_strip(G,j) = { |[r,s]| : G*(1
  ,j)`2 < s & s < G*(1,j+1)`2 };

theorem :: GOBOARD6:18
  Int cell(G,0,0) = { |[r,s]| : r < G*(1,1)`1 & s < G*(1,1)`2 };

theorem :: GOBOARD6:19
  Int cell(G,0,width G) = { |[r,s]| : r < G*(1,1)`1 & G*(1,width G )`2 < s };

theorem :: GOBOARD6:20
  1 <= j & j < width G implies Int cell(G,0,j) = { |[r,s]| : r < G
  *(1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 };

theorem :: GOBOARD6:21
  Int cell(G,len G,0) = { |[r,s]| : G*(len G,1)`1 < r & s < G*(1,1 )`2 };

theorem :: GOBOARD6:22
  Int cell(G,len G,width G) = { |[r,s]| : G*(len G,1)`1 < r & G*(1
  ,width G)`2 < s };

theorem :: GOBOARD6:23
  1 <= j & j < width G implies Int cell(G,len G,j) = { |[r,s]| : G
  *(len G,1)`1 < r & G*(1,j)`2 < s & s < G*(1,j+1)`2 };

theorem :: GOBOARD6:24
  1 <= i & i < len G implies Int cell(G,i,0) = { |[r,s]| : G*(i,1)
  `1 < r & r < G*(i+1,1)`1 & s < G*(1,1)`2 };

theorem :: GOBOARD6:25
  1 <= i & i < len G implies Int cell(G,i,width G) = { |[r,s]| : G
  *(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,width G)`2 < s };

theorem :: GOBOARD6:26
  1 <= i & i < len G & 1 <= j & j < width G implies Int cell(G,i,j
) = { |[r,s]| : G*(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)
  `2 };

theorem :: GOBOARD6:27
  1 <= j & j <= width G & p in Int h_strip(G,j) implies p`2 > G*(1,j)`2;

theorem :: GOBOARD6:28
  j < width G & p in Int h_strip(G,j) implies p`2 < G*(1,j+1)`2;

theorem :: GOBOARD6:29
  1 <= i & i <= len G & p in Int v_strip(G,i) implies p`1 > G*(i,1)`1;

theorem :: GOBOARD6:30
  i < len G & p in Int v_strip(G,i) implies p`1 < G*(i+1,1)`1;

theorem :: GOBOARD6:31
  1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies 1/2*(G*(
  i,j)+G*(i+1,j+1)) in Int cell(G,i,j);

theorem :: GOBOARD6:32
  1 <= i & i+1 <= len G implies 1/2*(G*(i,width G)+G*(i+1,width G)
  )+|[0,1]| in Int cell(G,i,width G);

theorem :: GOBOARD6:33
  1 <= i & i+1 <= len G implies 1/2*(G*(i,1)+G*(i+1,1))-|[0,1]| in
  Int cell(G,i,0);

theorem :: GOBOARD6:34
  1 <= j & j+1 <= width G implies 1/2*(G*(len G,j)+G*(len G,j+1))+
  |[1,0]| in Int cell(G,len G,j);

theorem :: GOBOARD6:35
  1 <= j & j+1 <= width G implies 1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|
  in Int cell(G,0,j);

theorem :: GOBOARD6:36
  G*(1,1)-|[1,1]| in Int cell(G,0,0);

theorem :: GOBOARD6:37
  G*(len G,width G)+|[1,1]| in Int cell(G,len G,width G);

theorem :: GOBOARD6:38
  G*(1,width G)+|[-1,1]| in Int cell(G,0,width G);

theorem :: GOBOARD6:39
  G*(len G,1)+|[1,-1]| in Int cell(G,len G,0);

theorem :: GOBOARD6:40
  1 <= i & i < len G & 1 <= j & j < width G implies LSeg(1/2*(G*(i
,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i,j+1))) c= Int cell(G,i,j) \/ { 1/2*(G*(i,j)+
  G*(i,j+1)) };

theorem :: GOBOARD6:41
  1 <= i & i < len G & 1 <= j & j < width G implies LSeg(1/2*(G*(i
,j)+G*(i+1,j+1)),1/2*(G*(i,j+1)+G*(i+1,j+1))) c= Int cell(G,i,j) \/ { 1/2*(G*(i
  ,j+1)+G*(i+1,j+1)) };

theorem :: GOBOARD6:42
  1 <= i & i < len G & 1 <= j & j < width G implies LSeg(1/2*(G*(i
,j)+G*(i+1,j+1)),1/2*(G*(i+1,j)+G*(i+1,j+1))) c= Int cell(G,i,j) \/ { 1/2*(G*(i
  +1,j)+G*(i+1,j+1)) };

theorem :: GOBOARD6:43
  1 <= i & i < len G & 1 <= j & j < width G implies LSeg(1/2*(G*(i
,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i+1,j))) c= Int cell(G,i,j) \/ { 1/2*(G*(i,j)+
  G*(i+1,j)) };

theorem :: GOBOARD6:44
  1 <= j & j < width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,
0]|,1/2*(G*(1,j)+G*(1,j+1))) c= Int cell(G,0,j) \/ { 1/2*(G*(1,j)+G*(1,j+1)) };

theorem :: GOBOARD6:45
  1 <= j & j < width G implies LSeg(1/2*(G*(len G,j)+G*(len G,j+1)
) + |[1,0]|,1/2*(G*(len G,j)+G*(len G,j+1))) c= Int cell(G,len G,j) \/ { 1/2*(G
  *(len G,j)+G*(len G,j+1)) };

theorem :: GOBOARD6:46
  1 <= i & i < len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1
  ]|,1/2*(G*(i,1)+G*(i+1,1))) c= Int cell(G,i,0) \/ { 1/2*(G*(i,1)+G*(i+1,1)) }
;

theorem :: GOBOARD6:47
  1 <= i & i < len G implies LSeg(1/2*(G*(i,width G)+G*(i+1,width
G))+ |[0,1]|, 1/2*(G*(i,width G)+G*(i+1,width G))) c= Int cell(G,i,width G) \/
  { 1/2*(G*(i,width G)+G*(i+1,width G)) };

theorem :: GOBOARD6:48
  1 <= j & j < width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,
  0]|,G*(1,j) - |[1,0]|) c= Int cell(G,0,j) \/ { G*(1,j) - |[1,0]| };

theorem :: GOBOARD6:49
  1 <= j & j < width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1,
  0]|,G*(1,j+1) - |[1,0]|) c= Int cell(G,0,j) \/ { G*(1,j+1) - |[1,0]| };

theorem :: GOBOARD6:50
  1 <= j & j < width G implies LSeg(1/2*(G*(len G,j)+G*(len G,j+1)
) + |[1,0]|,G*(len G,j) + |[1,0]|) c= Int cell(G,len G,j) \/ { G*(len G,j) + |[
  1,0]| };

theorem :: GOBOARD6:51
  1 <= j & j < width G implies LSeg(1/2*(G*(len G,j)+G*(len G,j+1)
) + |[1,0]|,G*(len G,j+1) + |[1,0]|) c= Int cell(G,len G,j) \/ { G*(len G,j+1)
  + |[1,0]| };

theorem :: GOBOARD6:52
  1 <= i & i < len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1
  ]|,G*(i,1) - |[0,1]|) c= Int cell(G,i,0) \/ { G*(i,1) - |[0,1]| };

theorem :: GOBOARD6:53
  1 <= i & i < len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1
  ]|,G*(i+1,1) - |[0,1]|) c= Int cell(G,i,0) \/ { G*(i+1,1) - |[0,1]| };

theorem :: GOBOARD6:54
  1 <= i & i < len G implies LSeg(1/2*(G*(i,width G)+G*(i+1,width
  G)) + |[0,1]|,G* (i,width G) + |[0,1]|) c= Int cell(G,i,width G) \/ { G*(i,
  width G) + |[0,1]| };

theorem :: GOBOARD6:55
  1 <= i & i < len G implies LSeg(1/2*(G*(i,width G)+G*(i+1,width
G)) + |[0,1]|,G* (i+1,width G) + |[0,1]|) c= Int cell(G,i,width G) \/ { G*(i+1,
  width G) + |[0,1]| };

theorem :: GOBOARD6:56
  LSeg(G*(1,1) - |[1,1]|,G*(1,1) - |[1,0]|) c= Int cell(G,0,0) \/
  { G*(1,1) - |[1,0]| };

theorem :: GOBOARD6:57
  LSeg(G*(len G,1) + |[1,-1]|,G*(len G,1) + |[1,0]|) c= Int cell(G
  ,len G,0) \/ { G*(len G,1) + |[1,0]| };

theorem :: GOBOARD6:58
  LSeg(G*(1,width G) + |[-1,1]|,G*(1,width G) - |[1,0]|) c= Int
  cell(G,0,width G) \/ { G*(1,width G) - |[1,0]| };

theorem :: GOBOARD6:59
  LSeg(G*(len G,width G) + |[1,1]|,G*(len G,width G) + |[1,0]|) c=
  Int cell(G,len G,width G) \/ { G*(len G,width G) + |[1,0]| };

theorem :: GOBOARD6:60
  LSeg(G*(1,1) - |[1,1]|,G*(1,1) - |[0,1]|) c= Int cell(G,0,0) \/
  { G*(1,1) - |[0,1]| };

theorem :: GOBOARD6:61
  LSeg(G*(len G,1) + |[1,-1]|,G*(len G,1) - |[0,1]|) c= Int cell(G
  ,len G,0) \/ { G*(len G,1) - |[0,1]| };

theorem :: GOBOARD6:62
  LSeg(G*(1,width G) + |[-1,1]|,G*(1,width G) + |[0,1]|) c= Int
  cell(G,0,width G) \/ { G*(1,width G) + |[0,1]| };

theorem :: GOBOARD6:63
  LSeg(G*(len G,width G) + |[1,1]|,G*(len G,width G) + |[0,1]|) c=
  Int cell(G,len G,width G) \/ { G*(len G,width G) + |[0,1]| };

theorem :: GOBOARD6:64
  1 <= i & i < len G & 1 <= j & j+1 < width G implies LSeg(1/2*(G*(i,j)+
G*(i+1,j+1)),1/2*(G*(i,j+1)+G*(i+1,j+2))) c= Int cell(G,i,j) \/ Int cell(G,i,j+
  1) \/ { 1/2*(G*(i,j+1)+G*(i+1,j+1)) };

theorem :: GOBOARD6:65
  1 <= j & j < width G & 1 <= i & i+1 < len G implies LSeg(1/2*(G*(i,j)+
G*(i+1,j+1)),1/2*(G*(i+1,j)+G*(i+2,j+1))) c= Int cell(G,i,j) \/ Int cell(G,i+1,
  j) \/ { 1/2*(G*(i+1,j)+G*(i+1,j+1)) };

theorem :: GOBOARD6:66
  1 <= i & i < len G & 1 < width G implies LSeg(1/2*(G*(i,1)+G*(i+1,1))-
|[0,1]|,1/2*(G*(i,1)+G*(i+1,2))) c= Int cell(G,i,0) \/ Int cell(G,i,1) \/ { 1/2
  *(G*(i,1)+G*(i+1,1)) };

theorem :: GOBOARD6:67
  1 <= i & i < len G & 1 < width G implies LSeg(1/2*(G*(i,width G)+G*(i+
1,width G))+|[0,1]|, 1/2*(G*(i,width G)+G*(i+1,width G -' 1))) c= Int cell(G,i,
width G -'1) \/ Int cell(G,i,width G) \/ { 1/2*(G*(i,width G)+G*(i+1,width G))
  };

theorem :: GOBOARD6:68
  1 <= j & j < width G & 1 < len G implies LSeg(1/2*(G*(1,j)+G*(1,j+1))-
|[1,0]|,1/2*(G*(1,j)+G*(2,j+1))) c= Int cell(G,0,j) \/ Int cell(G,1,j) \/ { 1/2
  *(G*(1,j)+G*(1,j+1)) };

theorem :: GOBOARD6:69
  1 <= j & j < width G & 1 < len G implies LSeg(1/2*(G*(len G,j)+G*(len
G,j+1))+|[1,0]|, 1/2*(G*(len G,j)+G*(len G -' 1,j+1))) c= Int cell(G,len G -' 1
  ,j) \/ Int cell(G,len G,j) \/ { 1/2*(G*(len G,j)+G*(len G,j+1)) };

theorem :: GOBOARD6:70
  1 < len G & 1 <= j & j+1 < width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1)
)-|[1,0]|,1/2*(G*(1,j+1)+G*(1,j+2))-|[1,0]|) c= Int cell(G,0,j) \/ Int cell(G,0
  ,j+1) \/ { G*(1,j+1)-|[1,0]| };

theorem :: GOBOARD6:71
  1 < len G & 1 <= j & j+1 < width G implies LSeg(1/2*(G*(len G,j)+G*(
len G,j+1))+|[1,0]|, 1/2*(G*(len G,j+1)+G*(len G,j+2))+|[1,0]|) c= Int cell(G,
  len G,j) \/ Int cell(G,len G,j+1) \/ { G*(len G,j+1)+|[1,0]| };

theorem :: GOBOARD6:72
  1 < width G & 1 <= i & i+1 < len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1)
)-|[0,1]|,1/2*(G*(i+1,1)+G*(i+2,1))-|[0,1]|) c= Int cell(G,i,0) \/ Int cell(G,i
  +1,0) \/ { G*(i+1,1)-|[0,1]| };

theorem :: GOBOARD6:73
  1 < width G & 1 <= i & i+1 < len G implies LSeg(1/2*(G*(i,width G)+G*(
  i+1,width G))+|[0,1]|, 1/2*(G*(i+1,width G)+G*(i+2,width G))+|[0,1]|) c= Int
  cell(G,i,width G) \/ Int cell(G,i+1,width G) \/ { G*(i+1,width G)+|[0,1]| };

theorem :: GOBOARD6:74
  1 < len G & 1 < width G implies LSeg(G*(1,1)-|[1,1]|,1/2*(G*(1,1)+G*(1
  ,2))-|[1,0]|) c= Int cell(G,0,0) \/ Int cell(G,0,1) \/ { G*(1,1)-|[1,0]| };

theorem :: GOBOARD6:75
  1 < len G & 1 < width G implies LSeg(G*(len G,1)+|[1,-1]|,1/2*(G*(len
G,1)+G*(len G,2))+|[1,0]|) c= Int cell(G,len G,0) \/ Int cell(G,len G,1) \/ { G
  *(len G,1)+|[1,0]| };

theorem :: GOBOARD6:76
  1 < len G & 1 < width G implies LSeg(G*(1,width G)+|[-1,1]|,1/2*(G*(1,
width G)+G* (1,width G -' 1))-|[1,0]|) c= Int cell(G,0,width G) \/ Int cell(G,0
  ,width G -' 1) \/ { G*(1,width G)-|[1,0]| };

theorem :: GOBOARD6:77
  1 < len G & 1 < width G implies LSeg(G*(len G,width G)+|[1,1]|, 1/2*(G
*(len G,width G)+G*(len G,width G -' 1))+|[1,0]|) c= Int cell(G,len G,width G)
  \/ Int cell(G,len G,width G -' 1) \/ { G*(len G,width G)+|[1,0]| };

theorem :: GOBOARD6:78
  1 < width G & 1 < len G implies LSeg(G*(1,1)-|[1,1]|,1/2*(G*(1,1)+G*(2
  ,1))-|[0,1]|) c= Int cell(G,0,0) \/ Int cell(G,1,0) \/ { G*(1,1)-|[0,1]| };

theorem :: GOBOARD6:79
  1 < width G & 1 < len G implies LSeg(G*(1,width G)+|[-1,1]|,1/2*(G*(1,
width G)+G*(2,width G))+|[0,1]|) c= Int cell(G,0,width G) \/ Int cell(G,1,width
  G) \/ { G*(1,width G)+|[0,1]| };

theorem :: GOBOARD6:80
  1 < width G & 1 < len G implies LSeg(G*(len G,1)+|[1,-1]|,1/2*(G*(len
G,1)+G*(len G -' 1,1))-|[0,1]|) c= Int cell(G,len G,0) \/ Int cell(G,len G -' 1
  ,0) \/ { G*(len G,1)-|[0,1]| };

theorem :: GOBOARD6:81
  1 < width G & 1 < len G implies LSeg(G*(len G,width G)+|[1,1]|, 1/2*(G
*(len G,width G)+G*(len G -' 1,width G))+|[0,1]|) c= Int cell(G,len G,width G)
  \/ Int cell(G,len G -' 1,width G) \/ { G*(len G,width G)+|[0,1]| };

theorem :: GOBOARD6:82
  1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(1/2*(G*(i
  ,j)+G*(i+1,j+1)),p) meets Int cell(G,i,j);

theorem :: GOBOARD6:83
  1 <= i & i+1 <= len G implies LSeg(p,1/2*(G*(i,width G)+G*(i+1,width G
  ))+|[0,1]|) meets Int cell(G,i,width G);

theorem :: GOBOARD6:84
  1 <= i & i+1 <= len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|,p)
  meets Int cell(G,i,0);

theorem :: GOBOARD6:85
  1 <= j & j+1 <= width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|,p
  ) meets Int cell(G,0,j);

theorem :: GOBOARD6:86
  1 <= j & j+1 <= width G implies LSeg(p,1/2*(G*(len G,j)+G*(len G,j+1))
  +|[1,0]|) meets Int cell(G,len G,j);

theorem :: GOBOARD6:87
  LSeg(p,G*(1,1)-|[1,1]|) meets Int cell(G,0,0);

theorem :: GOBOARD6:88
  LSeg(p,G*(len G,width G)+|[1,1]|) meets Int cell(G,len G,width G);

theorem :: GOBOARD6:89
  LSeg(p,G*(1,width G)+|[-1,1]|) meets Int cell(G,0,width G);

theorem :: GOBOARD6:90
  LSeg(p,G*(len G,1)+|[1,-1]|) meets Int cell(G,len G,0);

theorem :: GOBOARD6:91
  for M being non empty MetrSpace, p being Point of M, q being
Point of TopSpaceMetr M, r being Real st p = q & r > 0 holds Ball (p, r)
  is a_neighborhood of q;

theorem :: GOBOARD6:92
  for M being non empty MetrSpace, A being Subset of TopSpaceMetr M, p
  being Point of M holds p in Cl A iff for r being Real st r > 0 holds
  Ball (p, r) meets A;

:: Moved from JORDAN19, AG 20.01.2006

theorem :: GOBOARD6:93
  for A be Subset of TOP-REAL n for p be Point of TOP-REAL n for p9 be
  Point of Euclid n st p = p9 for s be Real st s > 0 holds p in Cl A iff
  for r be Real st 0 < r & r < s holds Ball (p9,r) meets A;