let G be Go-board; :: thesis: for j, k, j1, k1 being Element of 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)
let j, k, j1, k1 be Element of NAT ; :: thesis: ( 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G implies LSeg (G * (Center G),j1),(G * (Center G),k1) c= LSeg (G * (Center G),j),(G * (Center G),k) )
assume A1: ( 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G ) ; :: thesis: LSeg (G * (Center G),j1),(G * (Center G),k1) c= LSeg (G * (Center G),j),(G * (Center G),k)
( 1 <= Center G & Center G <= len G ) by JORDAN1B:12, JORDAN1B:14;
hence LSeg (G * (Center G),j1),(G * (Center G),k1) c= LSeg (G * (Center G),j),(G * (Center G),k) by A1, Th7; :: thesis: verum