let G be Go-board; :: thesis: 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)))
let j, k, j1, k1 be 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 that
A1: 1 <= j and
A2: j <= j1 and
A3: j1 <= k1 and
A4: k1 <= k and
A5: k <= width G ; :: thesis: LSeg ((G * ((Center G),j1)),(G * ((Center G),k1))) c= LSeg ((G * ((Center G),j)),(G * ((Center G),k)))
A6: Center G <= len G by JORDAN1B:13;
1 <= Center G by JORDAN1B:11;
hence LSeg ((G * ((Center G),j1)),(G * ((Center G),k1))) c= LSeg ((G * ((Center G),j)),(G * ((Center G),k))) by A1, A2, A3, A4, A5, A6, Th5; :: thesis: verum