theorem :: JORDAN15:8

for G being Go-board st len G = width G holds
for j, k, j1, k1 being Nat st 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg ((G * (j1,(Center G))),(G * (k1,(Center G)))) c= LSeg ((G * (j,(Center G))),(G * (k,(Center G))))