theorem Th21: :: GOBOARD5:21

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