theorem
for
G being
Go-board for
i1,
j1,
i2,
j2 being
Nat st 1
<= i1 &
i1 + 1
<= len G & 1
<= j1 &
j1 <= width G & 1
<= i2 &
i2 + 1
<= len G & 1
<= j2 &
j2 <= width G &
LSeg (
(G * (i1,j1)),
(G * ((i1 + 1),j1)))
meets LSeg (
(G * (i2,j2)),
(G * ((i2 + 1),j2))) & not (
i1 = i2 &
LSeg (
(G * (i1,j1)),
(G * ((i1 + 1),j1)))
= LSeg (
(G * (i2,j2)),
(G * ((i2 + 1),j2))) ) & not (
i1 = i2 + 1 &
(LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i1,j1))} ) holds
(
i1 + 1
= i2 &
(LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) /\ (LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2)))) = {(G * (i2,j2))} )