:: On the Geometry of a Go-board
:: by Andrzej Trybulec
::
:: Received July 9, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

Lm1: for p, q being Point of (TOP-REAL 2) holds
( (p + q) `1 = (p `1) + (q `1) & (p + q) `2 = (p `2) + (q `2) )
proof end;

Lm2: for p, q being Point of (TOP-REAL 2) holds
( (p - q) `1 = (p `1) - (q `1) & (p - q) `2 = (p `2) - (q `2) )
proof end;

Lm3: for r being Real
for p being Point of (TOP-REAL 2) holds
( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) )
proof end;

theorem Th1: :: GOBOARD6:1
for M being non empty Reflexive MetrStruct
for u being Point of M
for r being real number st r > 0 holds
u in Ball (u,r)
proof end;

Lm4: for M being MetrSpace
for B being Subset of (TopSpaceMetr M)
for r being real number
for u being Point of M st B = Ball (u,r) holds
B is open
proof end;

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

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

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

Lm5: for T being TopSpace
for A being Subset of T
for B being Subset of TopStruct(# the carrier of T, the topology of T #) st A = B holds
Int A = Int B
proof end;

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

theorem Th6: :: GOBOARD6:6
for r1, s1, r2, s2 being Real
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 Th7: :: GOBOARD6:7
for r, s, r2, r1 being Real
for u being Point of (Euclid 2) st u = |[r,s]| & 0 <= r2 & r2 < r1 holds
|[(r + r2),s]| in Ball (u,r1)
proof end;

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

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

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

theorem Th11: :: GOBOARD6:11
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
(G * (i,j)) + (G * ((i + 1),(j + 1))) = (G * (i,(j + 1))) + (G * ((i + 1),j))
proof end;

Lm6: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def 8
.= TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) by PCOMPS_1:def 5 ;

theorem Th12: :: GOBOARD6:12
for G being Go-board holds Int (v_strip (G,0)) = { |[r,s]| where r, s is Real : r < (G * (1,1)) `1 }
proof end;

theorem Th13: :: GOBOARD6:13
for G being Go-board holds Int (v_strip (G,(len G))) = { |[r,s]| where r, s is Real : (G * ((len G),1)) `1 < r }
proof end;

theorem Th14: :: GOBOARD6:14
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
Int (v_strip (G,i)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) }
proof end;

theorem Th15: :: GOBOARD6:15
for G being Go-board holds Int (h_strip (G,0)) = { |[r,s]| where r, s is Real : s < (G * (1,1)) `2 }
proof end;

theorem Th16: :: GOBOARD6:16
for G being Go-board holds Int (h_strip (G,(width G))) = { |[r,s]| where r, s is Real : (G * (1,(width G))) `2 < s }
proof end;

theorem Th17: :: GOBOARD6:17
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
Int (h_strip (G,j)) = { |[r,s]| where r, s is Real : ( (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
proof end;

theorem Th18: :: GOBOARD6:18
for G being Go-board holds Int (cell (G,0,0)) = { |[r,s]| where r, s is Real : ( r < (G * (1,1)) `1 & s < (G * (1,1)) `2 ) }
proof end;

theorem Th19: :: GOBOARD6:19
for G being Go-board holds Int (cell (G,0,(width G))) = { |[r,s]| where r, s is Real : ( r < (G * (1,1)) `1 & (G * (1,(width G))) `2 < s ) }
proof end;

theorem Th20: :: GOBOARD6:20
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
Int (cell (G,0,j)) = { |[r,s]| where r, s is Real : ( r < (G * (1,1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
proof end;

theorem Th21: :: GOBOARD6:21
for G being Go-board holds Int (cell (G,(len G),0)) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 < r & s < (G * (1,1)) `2 ) }
proof end;

theorem Th22: :: GOBOARD6:22
for G being Go-board holds Int (cell (G,(len G),(width G))) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 < r & (G * (1,(width G))) `2 < s ) }
proof end;

theorem Th23: :: GOBOARD6:23
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
Int (cell (G,(len G),j)) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 < r & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
proof end;

theorem Th24: :: GOBOARD6:24
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
Int (cell (G,i,0)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & s < (G * (1,1)) `2 ) }
proof end;

theorem Th25: :: GOBOARD6:25
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
Int (cell (G,i,(width G))) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,(width G))) `2 < s ) }
proof end;

theorem Th26: :: GOBOARD6:26
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
Int (cell (G,i,j)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
proof end;

theorem :: GOBOARD6:27
for j being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= j & j <= width G & p in Int (h_strip (G,j)) holds
p `2 > (G * (1,j)) `2
proof end;

theorem :: GOBOARD6:28
for j being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st j < width G & p in Int (h_strip (G,j)) holds
p `2 < (G * (1,(j + 1))) `2
proof end;

theorem :: GOBOARD6:29
for i being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= i & i <= len G & p in Int (v_strip (G,i)) holds
p `1 > (G * (i,1)) `1
proof end;

theorem :: GOBOARD6:30
for i being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st i < len G & p in Int (v_strip (G,i)) holds
p `1 < (G * ((i + 1),1)) `1
proof end;

theorem Th31: :: GOBOARD6:31
for i, j being Element of NAT
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
(1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in Int (cell (G,i,j))
proof end;

theorem Th32: :: GOBOARD6:32
for i being Element of NAT
for G being Go-board st 1 <= i & i + 1 <= len G holds
((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]| in Int (cell (G,i,(width G)))
proof end;

theorem Th33: :: GOBOARD6:33
for i being Element of NAT
for G being Go-board st 1 <= i & i + 1 <= len G holds
((1 / 2) * ((G * (i,1)) + (G * ((i + 1),1)))) - |[0,1]| in Int (cell (G,i,0))
proof end;

theorem Th34: :: GOBOARD6:34
for j being Element of NAT
for G being Go-board st 1 <= j & j + 1 <= width G holds
((1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1))))) + |[1,0]| in Int (cell (G,(len G),j))
proof end;

theorem Th35: :: GOBOARD6:35
for j being Element of NAT
for G being Go-board st 1 <= j & j + 1 <= width G holds
((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]| in Int (cell (G,0,j))
proof end;

theorem Th36: :: GOBOARD6:36
for G being Go-board holds (G * (1,1)) - |[1,1]| in Int (cell (G,0,0))
proof end;

theorem Th37: :: GOBOARD6:37
for G being Go-board holds (G * ((len G),(width G))) + |[1,1]| in Int (cell (G,(len G),(width G)))
proof end;

theorem Th38: :: GOBOARD6:38
for G being Go-board holds (G * (1,(width G))) + |[(- 1),1]| in Int (cell (G,0,(width G)))
proof end;

theorem Th39: :: GOBOARD6:39
for G being Go-board holds (G * ((len G),1)) + |[1,(- 1)]| in Int (cell (G,(len G),0))
proof end;

theorem Th40: :: GOBOARD6:40
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
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)))))}
proof end;

theorem Th41: :: GOBOARD6:41
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
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)))))}
proof end;

theorem Th42: :: GOBOARD6:42
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
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)))))}
proof end;

theorem Th43: :: GOBOARD6:43
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
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))))}
proof end;

theorem Th44: :: GOBOARD6:44
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
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)))))}
proof end;

theorem Th45: :: GOBOARD6:45
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
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)))))}
proof end;

theorem Th46: :: GOBOARD6:46
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
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))))}
proof end;

theorem Th47: :: GOBOARD6:47
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
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)))))}
proof end;

theorem Th48: :: GOBOARD6:48
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
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]|)}
proof end;

theorem Th49: :: GOBOARD6:49
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
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]|)}
proof end;

theorem Th50: :: GOBOARD6:50
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
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]|)}
proof end;

theorem Th51: :: GOBOARD6:51
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G holds
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]|)}
proof end;

theorem Th52: :: GOBOARD6:52
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
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]|)}
proof end;

theorem Th53: :: GOBOARD6:53
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
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]|)}
proof end;

theorem Th54: :: GOBOARD6:54
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
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]|)}
proof end;

theorem Th55: :: GOBOARD6:55
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G holds
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]|)}
proof end;

theorem Th56: :: GOBOARD6:56
for G being Go-board holds LSeg (((G * (1,1)) - |[1,1]|),((G * (1,1)) - |[1,0]|)) c= (Int (cell (G,0,0))) \/ {((G * (1,1)) - |[1,0]|)}
proof end;

theorem Th57: :: GOBOARD6:57
for G being Go-board holds 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]|)}
proof end;

theorem Th58: :: GOBOARD6:58
for G being Go-board holds 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]|)}
proof end;

theorem Th59: :: GOBOARD6:59
for G being Go-board holds 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]|)}
proof end;

theorem Th60: :: GOBOARD6:60
for G being Go-board holds LSeg (((G * (1,1)) - |[1,1]|),((G * (1,1)) - |[0,1]|)) c= (Int (cell (G,0,0))) \/ {((G * (1,1)) - |[0,1]|)}
proof end;

theorem Th61: :: GOBOARD6:61
for G being Go-board holds 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]|)}
proof end;

theorem Th62: :: GOBOARD6:62
for G being Go-board holds 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]|)}
proof end;

theorem Th63: :: GOBOARD6:63
for G being Go-board holds 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]|)}
proof end;

theorem :: GOBOARD6:64
for i, j being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 <= j & j + 1 < width G holds
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)))))}
proof end;

theorem :: GOBOARD6:65
for j, i being Element of NAT
for G being Go-board st 1 <= j & j < width G & 1 <= i & i + 1 < len G holds
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)))))}
proof end;

theorem :: GOBOARD6:66
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 < width G holds
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))))}
proof end;

theorem :: GOBOARD6:67
for i being Element of NAT
for G being Go-board st 1 <= i & i < len G & 1 < width G holds
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)))))}
proof end;

theorem :: GOBOARD6:68
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G & 1 < len G holds
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)))))}
proof end;

theorem :: GOBOARD6:69
for j being Element of NAT
for G being Go-board st 1 <= j & j < width G & 1 < len G holds
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)))))}
proof end;

Lm7: (1 / 2) + (1 / 2) = 1
;

theorem :: GOBOARD6:70
for j being Element of NAT
for G being Go-board st 1 < len G & 1 <= j & j + 1 < width G holds
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]|)}
proof end;

theorem :: GOBOARD6:71
for j being Element of NAT
for G being Go-board st 1 < len G & 1 <= j & j + 1 < width G holds
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]|)}
proof end;

theorem :: GOBOARD6:72
for i being Element of NAT
for G being Go-board st 1 < width G & 1 <= i & i + 1 < len G holds
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]|)}
proof end;

theorem :: GOBOARD6:73
for i being Element of NAT
for G being Go-board st 1 < width G & 1 <= i & i + 1 < len G holds
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]|)}
proof end;

theorem :: GOBOARD6:74
for G being Go-board st 1 < len G & 1 < width G holds
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]|)}
proof end;

theorem :: GOBOARD6:75
for G being Go-board st 1 < len G & 1 < width G holds
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]|)}
proof end;

theorem :: GOBOARD6:76
for G being Go-board st 1 < len G & 1 < width G holds
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]|)}
proof end;

theorem :: GOBOARD6:77
for G being Go-board st 1 < len G & 1 < width G holds
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]|)}
proof end;

theorem :: GOBOARD6:78
for G being Go-board st 1 < width G & 1 < len G holds
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]|)}
proof end;

theorem :: GOBOARD6:79
for G being Go-board st 1 < width G & 1 < len G holds
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]|)}
proof end;

theorem :: GOBOARD6:80
for G being Go-board st 1 < width G & 1 < len G holds
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]|)}
proof end;

theorem :: GOBOARD6:81
for G being Go-board st 1 < width G & 1 < len G holds
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]|)}
proof end;

theorem :: GOBOARD6:82
for i, j being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= i & i + 1 <= len G & 1 <= j & j + 1 <= width G holds
LSeg (((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))),p) meets Int (cell (G,i,j))
proof end;

theorem :: GOBOARD6:83
for i being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= i & i + 1 <= len G holds
LSeg (p,(((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|)) meets Int (cell (G,i,(width G)))
proof end;

theorem :: GOBOARD6:84
for i being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= i & i + 1 <= len G holds
LSeg ((((1 / 2) * ((G * (i,1)) + (G * ((i + 1),1)))) - |[0,1]|),p) meets Int (cell (G,i,0))
proof end;

theorem :: GOBOARD6:85
for j being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= j & j + 1 <= width G holds
LSeg ((((1 / 2) * ((G * (1,j)) + (G * (1,(j + 1))))) - |[1,0]|),p) meets Int (cell (G,0,j))
proof end;

theorem :: GOBOARD6:86
for j being Element of NAT
for p being Point of (TOP-REAL 2)
for G being Go-board st 1 <= j & j + 1 <= width G holds
LSeg (p,(((1 / 2) * ((G * ((len G),j)) + (G * ((len G),(j + 1))))) + |[1,0]|)) meets Int (cell (G,(len G),j))
proof end;

theorem :: GOBOARD6:87
for p being Point of (TOP-REAL 2)
for G being Go-board holds LSeg (p,((G * (1,1)) - |[1,1]|)) meets Int (cell (G,0,0))
proof end;

theorem :: GOBOARD6:88
for p being Point of (TOP-REAL 2)
for G being Go-board holds LSeg (p,((G * ((len G),(width G))) + |[1,1]|)) meets Int (cell (G,(len G),(width G)))
proof end;

theorem :: GOBOARD6:89
for p being Point of (TOP-REAL 2)
for G being Go-board holds LSeg (p,((G * (1,(width G))) + |[(- 1),1]|)) meets Int (cell (G,0,(width G)))
proof end;

theorem :: GOBOARD6:90
for p being Point of (TOP-REAL 2)
for G being Go-board holds LSeg (p,((G * ((len G),1)) + |[1,(- 1)]|)) meets Int (cell (G,(len G),0))
proof end;

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

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

:: Moved from JORDAN19, AG 20.01.2006
theorem :: GOBOARD6:93
for n being Nat
for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n)
for p9 being Point of (Euclid n) st p = p9 holds
for s being real number st s > 0 holds
( p in Cl A iff for r being real number st 0 < r & r < s holds
Ball (p9,r) meets A )
proof end;