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 <= len G & 1
<= j2 &
j2 + 1
<= width G &
LSeg (
(G * (i1,j1)),
(G * (i1,(j1 + 1))))
meets LSeg (
(G * (i2,j2)),
(G * (i2,(j2 + 1)))) & not (
j1 = j2 &
LSeg (
(G * (i1,j1)),
(G * (i1,(j1 + 1))))
= LSeg (
(G * (i2,j2)),
(G * (i2,(j2 + 1)))) ) & not (
j1 = j2 + 1 &
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = {(G * (i1,j1))} ) holds
(
j1 + 1
= j2 &
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1))))) = {(G * (i2,j2))} )