:: GOBOARD6 semantic presentation

Lemma1: for b1, b2 being Point of (TOP-REAL 2) holds
( (b1 + b2) `1 = (b1 `1 ) + (b2 `1 ) & (b1 + b2) `2 = (b1 `2 ) + (b2 `2 ) )
proof end;

Lemma2: for b1, b2 being Point of (TOP-REAL 2) holds
( (b1 - b2) `1 = (b1 `1 ) - (b2 `1 ) & (b1 - b2) `2 = (b1 `2 ) - (b2 `2 ) )
proof end;

Lemma3: for b1 being Real
for b2 being Point of (TOP-REAL 2) holds
( (b1 * b2) `1 = b1 * (b2 `1 ) & (b1 * b2) `2 = b1 * (b2 `2 ) )
proof end;

theorem Th1: :: GOBOARD6:1
canceled;

theorem Th2: :: GOBOARD6:2
canceled;

theorem Th3: :: GOBOARD6:3
canceled;

theorem Th4: :: GOBOARD6:4
for b1 being non empty Reflexive MetrStruct
for b2 being Point of b1
for b3 being real number st b3 > 0 holds
b2 in Ball b2,b3
proof end;

Lemma5: for b1 being MetrSpace
for b2 being Subset of (TopSpaceMetr b1)
for b3 being real number
for b4 being Point of b1 st b2 = Ball b4,b3 holds
b2 is open
proof end;

theorem Th5: :: GOBOARD6:5
canceled;

theorem Th6: :: GOBOARD6:6
for b1 being Nat
for b2 being Real
for b3 being Subset of (TOP-REAL b1)
for b4 being Point of (Euclid b1) st b3 = Ball b4,b2 holds
b3 is open by Lemma5;

theorem Th7: :: GOBOARD6:7
for b1 being non empty MetrSpace
for b2 being Point of b1
for b3 being Subset of (TopSpaceMetr b1) holds
( b2 in Int b3 iff ex b4 being real number st
( b4 > 0 & Ball b2,b4 c= b3 ) )
proof end;

theorem Th8: :: GOBOARD6:8
for b1 being Nat
for b2 being Point of (Euclid b1)
for b3 being Subset of (TOP-REAL b1) holds
( b2 in Int b3 iff ex b4 being real number st
( b4 > 0 & Ball b2,b4 c= b3 ) ) by Th7;

theorem Th9: :: GOBOARD6:9
for b1, b2, b3, b4 being Real
for b5, b6 being Point of (Euclid 2) st b5 = |[b1,b2]| & b6 = |[b3,b4]| holds
dist b5,b6 = sqrt (((b1 - b3) ^2 ) + ((b2 - b4) ^2 ))
proof end;

theorem Th10: :: GOBOARD6:10
for b1, b2, b3, b4 being Real
for b5 being Point of (Euclid 2) st b5 = |[b1,b2]| & 0 <= b3 & b3 < b4 holds
|[(b1 + b3),b2]| in Ball b5,b4
proof end;

theorem Th11: :: GOBOARD6:11
for b1, b2, b3, b4 being Real
for b5 being Point of (Euclid 2) st b5 = |[b1,b2]| & 0 <= b3 & b3 < b4 holds
|[b1,(b2 + b3)]| in Ball b5,b4
proof end;

theorem Th12: :: GOBOARD6:12
for b1, b2, b3, b4 being Real
for b5 being Point of (Euclid 2) st b5 = |[b1,b2]| & 0 <= b3 & b3 < b4 holds
|[(b1 - b3),b2]| in Ball b5,b4
proof end;

theorem Th13: :: GOBOARD6:13
for b1, b2, b3, b4 being Real
for b5 being Point of (Euclid 2) st b5 = |[b1,b2]| & 0 <= b3 & b3 < b4 holds
|[b1,(b2 - b3)]| in Ball b5,b4
proof end;

theorem Th14: :: GOBOARD6:14
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 < width b3 holds
(b3 * b1,b2) + (b3 * (b1 + 1),(b2 + 1)) = (b3 * b1,(b2 + 1)) + (b3 * (b1 + 1),b2)
proof end;

E15: 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 b1 being Go-board holds Int (v_strip b1,0) = { |[b2,b3]| where B is Real, B is Real : b2 < (b1 * 1,1) `1 }
proof end;

theorem Th16: :: GOBOARD6:16
for b1 being Go-board holds Int (v_strip b1,(len b1)) = { |[b2,b3]| where B is Real, B is Real : (b1 * (len b1),1) `1 < b2 }
proof end;

theorem Th17: :: GOBOARD6:17
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
Int (v_strip b2,b1) = { |[b3,b4]| where B is Real, B is Real : ( (b2 * b1,1) `1 < b3 & b3 < (b2 * (b1 + 1),1) `1 ) }
proof end;

theorem Th18: :: GOBOARD6:18
for b1 being Go-board holds Int (h_strip b1,0) = { |[b2,b3]| where B is Real, B is Real : b3 < (b1 * 1,1) `2 }
proof end;

theorem Th19: :: GOBOARD6:19
for b1 being Go-board holds Int (h_strip b1,(width b1)) = { |[b2,b3]| where B is Real, B is Real : (b1 * 1,(width b1)) `2 < b3 }
proof end;

theorem Th20: :: GOBOARD6:20
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
Int (h_strip b2,b1) = { |[b3,b4]| where B is Real, B is Real : ( (b2 * 1,b1) `2 < b4 & b4 < (b2 * 1,(b1 + 1)) `2 ) }
proof end;

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

theorem Th22: :: GOBOARD6:22
for b1 being Go-board holds Int (cell b1,0,(width b1)) = { |[b2,b3]| where B is Real, B is Real : ( b2 < (b1 * 1,1) `1 & (b1 * 1,(width b1)) `2 < b3 ) }
proof end;

theorem Th23: :: GOBOARD6:23
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
Int (cell b2,0,b1) = { |[b3,b4]| where B is Real, B is Real : ( b3 < (b2 * 1,1) `1 & (b2 * 1,b1) `2 < b4 & b4 < (b2 * 1,(b1 + 1)) `2 ) }
proof end;

theorem Th24: :: GOBOARD6:24
for b1 being Go-board holds Int (cell b1,(len b1),0) = { |[b2,b3]| where B is Real, B is Real : ( (b1 * (len b1),1) `1 < b2 & b3 < (b1 * 1,1) `2 ) }
proof end;

theorem Th25: :: GOBOARD6:25
for b1 being Go-board holds Int (cell b1,(len b1),(width b1)) = { |[b2,b3]| where B is Real, B is Real : ( (b1 * (len b1),1) `1 < b2 & (b1 * 1,(width b1)) `2 < b3 ) }
proof end;

theorem Th26: :: GOBOARD6:26
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
Int (cell b2,(len b2),b1) = { |[b3,b4]| where B is Real, B is Real : ( (b2 * (len b2),1) `1 < b3 & (b2 * 1,b1) `2 < b4 & b4 < (b2 * 1,(b1 + 1)) `2 ) }
proof end;

theorem Th27: :: GOBOARD6:27
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
Int (cell b2,b1,0) = { |[b3,b4]| where B is Real, B is Real : ( (b2 * b1,1) `1 < b3 & b3 < (b2 * (b1 + 1),1) `1 & b4 < (b2 * 1,1) `2 ) }
proof end;

theorem Th28: :: GOBOARD6:28
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
Int (cell b2,b1,(width b2)) = { |[b3,b4]| where B is Real, B is Real : ( (b2 * b1,1) `1 < b3 & b3 < (b2 * (b1 + 1),1) `1 & (b2 * 1,(width b2)) `2 < b4 ) }
proof end;

theorem Th29: :: GOBOARD6:29
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 < width b3 holds
Int (cell b3,b1,b2) = { |[b4,b5]| where B is Real, B is Real : ( (b3 * b1,1) `1 < b4 & b4 < (b3 * (b1 + 1),1) `1 & (b3 * 1,b2) `2 < b5 & b5 < (b3 * 1,(b2 + 1)) `2 ) }
proof end;

theorem Th30: :: GOBOARD6:30
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being Go-board st 1 <= b1 & b1 <= width b3 & b2 in Int (h_strip b3,b1) holds
b2 `2 > (b3 * 1,b1) `2
proof end;

theorem Th31: :: GOBOARD6:31
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being Go-board st b1 < width b3 & b2 in Int (h_strip b3,b1) holds
b2 `2 < (b3 * 1,(b1 + 1)) `2
proof end;

theorem Th32: :: GOBOARD6:32
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being Go-board st 1 <= b1 & b1 <= len b3 & b2 in Int (v_strip b3,b1) holds
b2 `1 > (b3 * b1,1) `1
proof end;

theorem Th33: :: GOBOARD6:33
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being Go-board st b1 < len b3 & b2 in Int (v_strip b3,b1) holds
b2 `1 < (b3 * (b1 + 1),1) `1
proof end;

theorem Th34: :: GOBOARD6:34
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 & 1 <= b2 & b2 + 1 <= width b3 holds
(1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),(b2 + 1))) in Int (cell b3,b1,b2)
proof end;

theorem Th35: :: GOBOARD6:35
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 + 1 <= len b2 holds
((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2)))) + |[0,1]| in Int (cell b2,b1,(width b2))
proof end;

theorem Th36: :: GOBOARD6:36
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 + 1 <= len b2 holds
((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1))) - |[0,1]| in Int (cell b2,b1,0)
proof end;

theorem Th37: :: GOBOARD6:37
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 + 1 <= width b2 holds
((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1)))) + |[1,0]| in Int (cell b2,(len b2),b1)
proof end;

theorem Th38: :: GOBOARD6:38
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 + 1 <= width b2 holds
((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1)))) - |[1,0]| in Int (cell b2,0,b1)
proof end;

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

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

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

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

theorem Th43: :: GOBOARD6:43
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 < width b3 holds
LSeg ((1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),(b2 + 1)))),((1 / 2) * ((b3 * b1,b2) + (b3 * b1,(b2 + 1)))) c= (Int (cell b3,b1,b2)) \/ {((1 / 2) * ((b3 * b1,b2) + (b3 * b1,(b2 + 1))))}
proof end;

theorem Th44: :: GOBOARD6:44
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 < width b3 holds
LSeg ((1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),(b2 + 1)))),((1 / 2) * ((b3 * b1,(b2 + 1)) + (b3 * (b1 + 1),(b2 + 1)))) c= (Int (cell b3,b1,b2)) \/ {((1 / 2) * ((b3 * b1,(b2 + 1)) + (b3 * (b1 + 1),(b2 + 1))))}
proof end;

theorem Th45: :: GOBOARD6:45
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 < width b3 holds
LSeg ((1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),(b2 + 1)))),((1 / 2) * ((b3 * (b1 + 1),b2) + (b3 * (b1 + 1),(b2 + 1)))) c= (Int (cell b3,b1,b2)) \/ {((1 / 2) * ((b3 * (b1 + 1),b2) + (b3 * (b1 + 1),(b2 + 1))))}
proof end;

theorem Th46: :: GOBOARD6:46
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 < width b3 holds
LSeg ((1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),(b2 + 1)))),((1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),b2))) c= (Int (cell b3,b1,b2)) \/ {((1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),b2)))}
proof end;

theorem Th47: :: GOBOARD6:47
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
LSeg (((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1)))) - |[1,0]|),((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1)))) c= (Int (cell b2,0,b1)) \/ {((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1))))}
proof end;

theorem Th48: :: GOBOARD6:48
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
LSeg (((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1)))) + |[1,0]|),((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1)))) c= (Int (cell b2,(len b2),b1)) \/ {((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1))))}
proof end;

theorem Th49: :: GOBOARD6:49
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
LSeg (((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1))) - |[0,1]|),((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1))) c= (Int (cell b2,b1,0)) \/ {((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1)))}
proof end;

theorem Th50: :: GOBOARD6:50
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
LSeg (((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2)))) + |[0,1]|),((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2)))) c= (Int (cell b2,b1,(width b2))) \/ {((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2))))}
proof end;

theorem Th51: :: GOBOARD6:51
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
LSeg (((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1)))) - |[1,0]|),((b2 * 1,b1) - |[1,0]|) c= (Int (cell b2,0,b1)) \/ {((b2 * 1,b1) - |[1,0]|)}
proof end;

theorem Th52: :: GOBOARD6:52
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
LSeg (((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1)))) - |[1,0]|),((b2 * 1,(b1 + 1)) - |[1,0]|) c= (Int (cell b2,0,b1)) \/ {((b2 * 1,(b1 + 1)) - |[1,0]|)}
proof end;

theorem Th53: :: GOBOARD6:53
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
LSeg (((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1)))) + |[1,0]|),((b2 * (len b2),b1) + |[1,0]|) c= (Int (cell b2,(len b2),b1)) \/ {((b2 * (len b2),b1) + |[1,0]|)}
proof end;

theorem Th54: :: GOBOARD6:54
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 holds
LSeg (((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1)))) + |[1,0]|),((b2 * (len b2),(b1 + 1)) + |[1,0]|) c= (Int (cell b2,(len b2),b1)) \/ {((b2 * (len b2),(b1 + 1)) + |[1,0]|)}
proof end;

theorem Th55: :: GOBOARD6:55
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
LSeg (((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1))) - |[0,1]|),((b2 * b1,1) - |[0,1]|) c= (Int (cell b2,b1,0)) \/ {((b2 * b1,1) - |[0,1]|)}
proof end;

theorem Th56: :: GOBOARD6:56
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
LSeg (((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1))) - |[0,1]|),((b2 * (b1 + 1),1) - |[0,1]|) c= (Int (cell b2,b1,0)) \/ {((b2 * (b1 + 1),1) - |[0,1]|)}
proof end;

theorem Th57: :: GOBOARD6:57
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
LSeg (((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2)))) + |[0,1]|),((b2 * b1,(width b2)) + |[0,1]|) c= (Int (cell b2,b1,(width b2))) \/ {((b2 * b1,(width b2)) + |[0,1]|)}
proof end;

theorem Th58: :: GOBOARD6:58
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 holds
LSeg (((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2)))) + |[0,1]|),((b2 * (b1 + 1),(width b2)) + |[0,1]|) c= (Int (cell b2,b1,(width b2))) \/ {((b2 * (b1 + 1),(width b2)) + |[0,1]|)}
proof end;

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

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

theorem Th61: :: GOBOARD6:61
for b1 being Go-board holds LSeg ((b1 * 1,(width b1)) + |[(- 1),1]|),((b1 * 1,(width b1)) - |[1,0]|) c= (Int (cell b1,0,(width b1))) \/ {((b1 * 1,(width b1)) - |[1,0]|)}
proof end;

theorem Th62: :: GOBOARD6:62
for b1 being Go-board holds LSeg ((b1 * (len b1),(width b1)) + |[1,1]|),((b1 * (len b1),(width b1)) + |[1,0]|) c= (Int (cell b1,(len b1),(width b1))) \/ {((b1 * (len b1),(width b1)) + |[1,0]|)}
proof end;

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

theorem Th64: :: GOBOARD6:64
for b1 being Go-board holds LSeg ((b1 * (len b1),1) + |[1,(- 1)]|),((b1 * (len b1),1) - |[0,1]|) c= (Int (cell b1,(len b1),0)) \/ {((b1 * (len b1),1) - |[0,1]|)}
proof end;

theorem Th65: :: GOBOARD6:65
for b1 being Go-board holds LSeg ((b1 * 1,(width b1)) + |[(- 1),1]|),((b1 * 1,(width b1)) + |[0,1]|) c= (Int (cell b1,0,(width b1))) \/ {((b1 * 1,(width b1)) + |[0,1]|)}
proof end;

theorem Th66: :: GOBOARD6:66
for b1 being Go-board holds LSeg ((b1 * (len b1),(width b1)) + |[1,1]|),((b1 * (len b1),(width b1)) + |[0,1]|) c= (Int (cell b1,(len b1),(width b1))) \/ {((b1 * (len b1),(width b1)) + |[0,1]|)}
proof end;

theorem Th67: :: GOBOARD6:67
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < len b3 & 1 <= b2 & b2 + 1 < width b3 holds
LSeg ((1 / 2) * ((b3 * b1,b2) + (b3 * (b1 + 1),(b2 + 1)))),((1 / 2) * ((b3 * b1,(b2 + 1)) + (b3 * (b1 + 1),(b2 + 2)))) c= ((Int (cell b3,b1,b2)) \/ (Int (cell b3,b1,(b2 + 1)))) \/ {((1 / 2) * ((b3 * b1,(b2 + 1)) + (b3 * (b1 + 1),(b2 + 1))))}
proof end;

theorem Th68: :: GOBOARD6:68
for b1, b2 being Nat
for b3 being Go-board st 1 <= b1 & b1 < width b3 & 1 <= b2 & b2 + 1 < len b3 holds
LSeg ((1 / 2) * ((b3 * b2,b1) + (b3 * (b2 + 1),(b1 + 1)))),((1 / 2) * ((b3 * (b2 + 1),b1) + (b3 * (b2 + 2),(b1 + 1)))) c= ((Int (cell b3,b2,b1)) \/ (Int (cell b3,(b2 + 1),b1))) \/ {((1 / 2) * ((b3 * (b2 + 1),b1) + (b3 * (b2 + 1),(b1 + 1))))}
proof end;

theorem Th69: :: GOBOARD6:69
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 & 1 < width b2 holds
LSeg (((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1))) - |[0,1]|),((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),2))) c= ((Int (cell b2,b1,0)) \/ (Int (cell b2,b1,1))) \/ {((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1)))}
proof end;

theorem Th70: :: GOBOARD6:70
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < len b2 & 1 < width b2 holds
LSeg (((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2)))) + |[0,1]|),((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),((width b2) -' 1)))) c= ((Int (cell b2,b1,((width b2) -' 1))) \/ (Int (cell b2,b1,(width b2)))) \/ {((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2))))}
proof end;

theorem Th71: :: GOBOARD6:71
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 & 1 < len b2 holds
LSeg (((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1)))) - |[1,0]|),((1 / 2) * ((b2 * 1,b1) + (b2 * 2,(b1 + 1)))) c= ((Int (cell b2,0,b1)) \/ (Int (cell b2,1,b1))) \/ {((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1))))}
proof end;

theorem Th72: :: GOBOARD6:72
for b1 being Nat
for b2 being Go-board st 1 <= b1 & b1 < width b2 & 1 < len b2 holds
LSeg (((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1)))) + |[1,0]|),((1 / 2) * ((b2 * (len b2),b1) + (b2 * ((len b2) -' 1),(b1 + 1)))) c= ((Int (cell b2,((len b2) -' 1),b1)) \/ (Int (cell b2,(len b2),b1))) \/ {((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1))))}
proof end;

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

theorem Th73: :: GOBOARD6:73
for b1 being Nat
for b2 being Go-board st 1 < len b2 & 1 <= b1 & b1 + 1 < width b2 holds
LSeg (((1 / 2) * ((b2 * 1,b1) + (b2 * 1,(b1 + 1)))) - |[1,0]|),(((1 / 2) * ((b2 * 1,(b1 + 1)) + (b2 * 1,(b1 + 2)))) - |[1,0]|) c= ((Int (cell b2,0,b1)) \/ (Int (cell b2,0,(b1 + 1)))) \/ {((b2 * 1,(b1 + 1)) - |[1,0]|)}
proof end;

theorem Th74: :: GOBOARD6:74
for b1 being Nat
for b2 being Go-board st 1 < len b2 & 1 <= b1 & b1 + 1 < width b2 holds
LSeg (((1 / 2) * ((b2 * (len b2),b1) + (b2 * (len b2),(b1 + 1)))) + |[1,0]|),(((1 / 2) * ((b2 * (len b2),(b1 + 1)) + (b2 * (len b2),(b1 + 2)))) + |[1,0]|) c= ((Int (cell b2,(len b2),b1)) \/ (Int (cell b2,(len b2),(b1 + 1)))) \/ {((b2 * (len b2),(b1 + 1)) + |[1,0]|)}
proof end;

theorem Th75: :: GOBOARD6:75
for b1 being Nat
for b2 being Go-board st 1 < width b2 & 1 <= b1 & b1 + 1 < len b2 holds
LSeg (((1 / 2) * ((b2 * b1,1) + (b2 * (b1 + 1),1))) - |[0,1]|),(((1 / 2) * ((b2 * (b1 + 1),1) + (b2 * (b1 + 2),1))) - |[0,1]|) c= ((Int (cell b2,b1,0)) \/ (Int (cell b2,(b1 + 1),0))) \/ {((b2 * (b1 + 1),1) - |[0,1]|)}
proof end;

theorem Th76: :: GOBOARD6:76
for b1 being Nat
for b2 being Go-board st 1 < width b2 & 1 <= b1 & b1 + 1 < len b2 holds
LSeg (((1 / 2) * ((b2 * b1,(width b2)) + (b2 * (b1 + 1),(width b2)))) + |[0,1]|),(((1 / 2) * ((b2 * (b1 + 1),(width b2)) + (b2 * (b1 + 2),(width b2)))) + |[0,1]|) c= ((Int (cell b2,b1,(width b2))) \/ (Int (cell b2,(b1 + 1),(width b2)))) \/ {((b2 * (b1 + 1),(width b2)) + |[0,1]|)}
proof end;

theorem Th77: :: GOBOARD6:77
for b1 being Go-board st 1 < len b1 & 1 < width b1 holds
LSeg ((b1 * 1,1) - |[1,1]|),(((1 / 2) * ((b1 * 1,1) + (b1 * 1,2))) - |[1,0]|) c= ((Int (cell b1,0,0)) \/ (Int (cell b1,0,1))) \/ {((b1 * 1,1) - |[1,0]|)}
proof end;

theorem Th78: :: GOBOARD6:78
for b1 being Go-board st 1 < len b1 & 1 < width b1 holds
LSeg ((b1 * (len b1),1) + |[1,(- 1)]|),(((1 / 2) * ((b1 * (len b1),1) + (b1 * (len b1),2))) + |[1,0]|) c= ((Int (cell b1,(len b1),0)) \/ (Int (cell b1,(len b1),1))) \/ {((b1 * (len b1),1) + |[1,0]|)}
proof end;

theorem Th79: :: GOBOARD6:79
for b1 being Go-board st 1 < len b1 & 1 < width b1 holds
LSeg ((b1 * 1,(width b1)) + |[(- 1),1]|),(((1 / 2) * ((b1 * 1,(width b1)) + (b1 * 1,((width b1) -' 1)))) - |[1,0]|) c= ((Int (cell b1,0,(width b1))) \/ (Int (cell b1,0,((width b1) -' 1)))) \/ {((b1 * 1,(width b1)) - |[1,0]|)}
proof end;

theorem Th80: :: GOBOARD6:80
for b1 being Go-board st 1 < len b1 & 1 < width b1 holds
LSeg ((b1 * (len b1),(width b1)) + |[1,1]|),(((1 / 2) * ((b1 * (len b1),(width b1)) + (b1 * (len b1),((width b1) -' 1)))) + |[1,0]|) c= ((Int (cell b1,(len b1),(width b1))) \/ (Int (cell b1,(len b1),((width b1) -' 1)))) \/ {((b1 * (len b1),(width b1)) + |[1,0]|)}
proof end;

theorem Th81: :: GOBOARD6:81
for b1 being Go-board st 1 < width b1 & 1 < len b1 holds
LSeg ((b1 * 1,1) - |[1,1]|),(((1 / 2) * ((b1 * 1,1) + (b1 * 2,1))) - |[0,1]|) c= ((Int (cell b1,0,0)) \/ (Int (cell b1,1,0))) \/ {((b1 * 1,1) - |[0,1]|)}
proof end;

theorem Th82: :: GOBOARD6:82
for b1 being Go-board st 1 < width b1 & 1 < len b1 holds
LSeg ((b1 * 1,(width b1)) + |[(- 1),1]|),(((1 / 2) * ((b1 * 1,(width b1)) + (b1 * 2,(width b1)))) + |[0,1]|) c= ((Int (cell b1,0,(width b1))) \/ (Int (cell b1,1,(width b1)))) \/ {((b1 * 1,(width b1)) + |[0,1]|)}
proof end;

theorem Th83: :: GOBOARD6:83
for b1 being Go-board st 1 < width b1 & 1 < len b1 holds
LSeg ((b1 * (len b1),1) + |[1,(- 1)]|),(((1 / 2) * ((b1 * (len b1),1) + (b1 * ((len b1) -' 1),1))) - |[0,1]|) c= ((Int (cell b1,(len b1),0)) \/ (Int (cell b1,((len b1) -' 1),0))) \/ {((b1 * (len b1),1) - |[0,1]|)}
proof end;

theorem Th84: :: GOBOARD6:84
for b1 being Go-board st 1 < width b1 & 1 < len b1 holds
LSeg ((b1 * (len b1),(width b1)) + |[1,1]|),(((1 / 2) * ((b1 * (len b1),(width b1)) + (b1 * ((len b1) -' 1),(width b1)))) + |[0,1]|) c= ((Int (cell b1,(len b1),(width b1))) \/ (Int (cell b1,((len b1) -' 1),(width b1)))) \/ {((b1 * (len b1),(width b1)) + |[0,1]|)}
proof end;

theorem Th85: :: GOBOARD6:85
for b1, b2 being Nat
for b3 being Point of (TOP-REAL 2)
for b4 being Go-board st 1 <= b1 & b1 + 1 <= len b4 & 1 <= b2 & b2 + 1 <= width b4 holds
LSeg ((1 / 2) * ((b4 * b1,b2) + (b4 * (b1 + 1),(b2 + 1)))),b3 meets Int (cell b4,b1,b2)
proof end;

theorem Th86: :: GOBOARD6:86
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 holds
LSeg b2,(((1 / 2) * ((b3 * b1,(width b3)) + (b3 * (b1 + 1),(width b3)))) + |[0,1]|) meets Int (cell b3,b1,(width b3))
proof end;

theorem Th87: :: GOBOARD6:87
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being Go-board st 1 <= b1 & b1 + 1 <= len b3 holds
LSeg (((1 / 2) * ((b3 * b1,1) + (b3 * (b1 + 1),1))) - |[0,1]|),b2 meets Int (cell b3,b1,0)
proof end;

theorem Th88: :: GOBOARD6:88
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being Go-board st 1 <= b1 & b1 + 1 <= width b3 holds
LSeg (((1 / 2) * ((b3 * 1,b1) + (b3 * 1,(b1 + 1)))) - |[1,0]|),b2 meets Int (cell b3,0,b1)
proof end;

theorem Th89: :: GOBOARD6:89
for b1 being Nat
for b2 being Point of (TOP-REAL 2)
for b3 being Go-board st 1 <= b1 & b1 + 1 <= width b3 holds
LSeg b2,(((1 / 2) * ((b3 * (len b3),b1) + (b3 * (len b3),(b1 + 1)))) + |[1,0]|) meets Int (cell b3,(len b3),b1)
proof end;

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

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

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

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