:: by Andrzej Trybulec

::

:: Received July 9, 1995

:: Copyright (c) 1995-2018 Association of Mizar Users

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 st r > 0 holds

u in Ball (u,r)

for u being Point of M

for r being Real 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

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 st p = q & r > 0 holds

Ball (p,r) is a_neighborhood of q

for p being Point of (Euclid n)

for q being Point of (TOP-REAL n)

for r being Real 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

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 st

( r > 0 & Ball (u,r) c= P ) )

for u being Point of M

for P being Subset of (TopSpaceMetr M) holds

( u in Int P iff ex r being Real 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 st

( r > 0 & Ball (u,r) c= P ) )

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 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))

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, r1, r2 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)

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, s1, s2 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)

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, r1, r2 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)

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, s1, s2 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)

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 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))

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 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 ) }

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 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 ) }

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 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 ) }

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 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 ) }

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 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 ) }

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 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 ) }

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 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 ) }

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

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

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

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

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 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))

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 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)))

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 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))

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 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))

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 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))

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 Th40: :: GOBOARD6:40

for i, j being 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)))))}

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 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)))))}

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 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)))))}

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 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))))}

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 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)))))}

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 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)))))}

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 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))))}

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 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)))))}

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 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]|)}

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 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]|)}

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 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]|)}

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 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]|)}

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 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]|)}

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 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]|)}

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 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]|)}

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 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]|)}

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 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)))))}

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 i, j being 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)))))}

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 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))))}

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 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)))))}

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 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)))))}

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 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)))))}

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 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]|)}

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 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]|)}

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 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]|)}

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 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]|)}

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]|)}

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]|)}

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]|)}

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]|)}

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]|)}

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]|)}

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]|)}

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]|)}

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 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))

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 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)))

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 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))

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 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))

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 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))

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))

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)))

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)))

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))

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 st p = q & r > 0 holds

Ball (p,r) is a_neighborhood of q

for p being Point of M

for q being Point of (TopSpaceMetr M)

for r being Real 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 st r > 0 holds

Ball (p,r) meets A )

for A being Subset of (TopSpaceMetr M)

for p being Point of M holds

( p in Cl A iff for r being Real 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 st s > 0 holds

( p in Cl A iff for r being Real st 0 < r & r < s holds

Ball (p9,r) meets A )

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 st s > 0 holds

( p in Cl A iff for r being Real st 0 < r & r < s holds

Ball (p9,r) meets A )

proof end;