theorem Th53: :: GOBOARD6:53

for i being Nat
for G being Go-board st 1 <= i & i < len G holds
LSeg ((((1 / 2) * ((G * (i,1)) + (G * ((i + 1),1)))) - |[0,1]|),((G * ((i + 1),1)) - |[0,1]|)) c= (Int (cell (G,i,0))) \/ {((G * ((i + 1),1)) - |[0,1]|)}