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