:: On the Geometry of a Go-board
:: by Andrzej Trybulec
::
:: Received July 9, 1995
:: Copyright (c) 1995 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 :: GOBOARD6:1

canceled;

theorem :: GOBOARD6:2

canceled;

theorem :: GOBOARD6:3

canceled;

theorem Th4: :: GOBOARD6:4

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 Th5: :: GOBOARD6:5

for n being Element of 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 Th6: :: GOBOARD6:6

for n being Element of 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 Th7: :: GOBOARD6:7

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 Th8: :: GOBOARD6:8

for n being Element of 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 Th9: :: GOBOARD6:9

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 Th10: :: GOBOARD6:10

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 Th11: :: GOBOARD6:11

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 Th12: :: GOBOARD6:12

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 Th13: :: GOBOARD6:13

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 Th14: :: GOBOARD6:14

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 6 ;

theorem Th15: :: GOBOARD6:15

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 Th16: :: GOBOARD6:16

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 Th17: :: GOBOARD6:17

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 Th18: :: GOBOARD6:18

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 Th19: :: GOBOARD6:19

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 Th20: :: GOBOARD6:20

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 Th21: :: GOBOARD6:21

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 Th22: :: GOBOARD6:22

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 Th23: :: GOBOARD6:23

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 Th24: :: GOBOARD6:24

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 Th25: :: GOBOARD6:25

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 Th26: :: GOBOARD6:26

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 Th27: :: GOBOARD6:27

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 Th28: :: GOBOARD6:28

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 Th29: :: GOBOARD6:29

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:30

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:31

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:32

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:33

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 Th34: :: GOBOARD6:34

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 Th35: :: GOBOARD6:35

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 Th36: :: GOBOARD6:36

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 Th37: :: GOBOARD6:37

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 Th38: :: GOBOARD6:38

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 Th39: :: GOBOARD6:39

for G being Go-board holds (G * (1,1)) - |[1,1]| in Int (cell (G,0,0))

proof end;

theorem Th40: :: GOBOARD6:40

for G being Go-board holds (G * ((len G),(width G))) + |[1,1]| in Int (cell (G,(len G),(width G)))

proof end;

theorem Th41: :: GOBOARD6:41

for G being Go-board holds (G * (1,(width G))) + |[(- 1),1]| in Int (cell (G,0,(width G)))

proof end;

theorem Th42: :: GOBOARD6:42

for G being Go-board holds (G * ((len G),1)) + |[1,(- 1)]| in Int (cell (G,(len G),0))

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,(j + 1)))))) c= (Int (cell (G,i,j))) \/ {((1 / 2) * ((G * (i,j)) + (G * (i,(j + 1)))))}

proof end;

theorem Th44: :: GOBOARD6:44

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 Th45: :: GOBOARD6:45

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 Th46: :: GOBOARD6:46

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 Th47: :: GOBOARD6:47

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 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 * ((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 Th49: :: GOBOARD6:49

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 Th50: :: GOBOARD6:50

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 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 * (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 Th52: :: GOBOARD6:52

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 Th53: :: GOBOARD6:53

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 Th54: :: GOBOARD6:54

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 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,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 Th56: :: GOBOARD6:56

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 Th57: :: GOBOARD6:57

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 Th58: :: GOBOARD6:58

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 Th59: :: GOBOARD6:59

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 Th60: :: GOBOARD6:60

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 Th61: :: GOBOARD6:61

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 Th62: :: GOBOARD6:62

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 Th63: :: GOBOARD6:63

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 Th64: :: GOBOARD6:64

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 Th65: :: GOBOARD6:65

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 Th66: :: GOBOARD6:66

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:67

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:68

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:69

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:70

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:71

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:72

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:73

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:74

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:75

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:76

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:77

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:78

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:79

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:80

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:81

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:82

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:83

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:84

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:85

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:86

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:87

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:88

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:89

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:90

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:91

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:92

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:93

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 Th94: :: GOBOARD6:94

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:95

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;

theorem :: GOBOARD6:96

for n being Element of 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;