let G be Go-board; :: thesis: ( len G = width G implies 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)))) )

assume len G = width G ; :: thesis: 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))))

then A1: Center G <= width G by JORDAN1B:13;

let j, k, j1, k1 be 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 that

A2: 1 <= j and

A3: j <= j1 and

A4: j1 <= k1 and

A5: k1 <= k and

A6: 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 by JORDAN1B:11;

hence LSeg ((G * (j1,(Center G))),(G * (k1,(Center G)))) c= LSeg ((G * (j,(Center G))),(G * (k,(Center G)))) by A2, A3, A4, A5, A6, A1, Th6; :: thesis: verum

LSeg ((G * (j1,(Center G))),(G * (k1,(Center G)))) c= LSeg ((G * (j,(Center G))),(G * (k,(Center G)))) )

assume len G = width G ; :: thesis: 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))))

then A1: Center G <= width G by JORDAN1B:13;

let j, k, j1, k1 be 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 that

A2: 1 <= j and

A3: j <= j1 and

A4: j1 <= k1 and

A5: k1 <= k and

A6: 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 by JORDAN1B:11;

hence LSeg ((G * (j1,(Center G))),(G * (k1,(Center G)))) c= LSeg ((G * (j,(Center G))),(G * (k,(Center G)))) by A2, A3, A4, A5, A6, A1, Th6; :: thesis: verum