:: 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 p' being Point of (Euclid n) st p = p' 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 p',r meets A )

proof end;