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