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