let G be Go-board; ( 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
; 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; ( 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
; 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; verum