theorem Th18: :: GOBOARD5:18

for i, j being Nat
for G being Go-board st i < len G & 1 <= j & j < width G holds
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)