let G be Go-board; :: thesis: for i, j, k, j1, k1 being Nat st 1 <= i & i <= len G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg ((G * (i,j1)),(G * (i,k1))) c= LSeg ((G * (i,j)),(G * (i,k)))

let i, j, k, j1, k1 be Nat; :: thesis: ( 1 <= i & i <= len G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G implies LSeg ((G * (i,j1)),(G * (i,k1))) c= LSeg ((G * (i,j)),(G * (i,k))) )
assume that
A1: 1 <= i and
A2: i <= len G and
A3: 1 <= j and
A4: j <= j1 and
A5: j1 <= k1 and
A6: k1 <= k and
A7: k <= width G ; :: thesis: LSeg ((G * (i,j1)),(G * (i,k1))) c= LSeg ((G * (i,j)),(G * (i,k)))
A8: j1 <= k by ;
j <= k1 by ;
then A9: 1 <= k1 by ;
then A10: (G * (i,k1)) `2 <= (G * (i,k)) `2 by ;
A11: 1 <= j1 by ;
1 <= j1 by ;
then A12: 1 <= k by ;
A13: k1 <= width G by ;
j <= k1 by ;
then A14: j <= width G by ;
then (G * (i,j)) `1 = (G * (i,1)) `1 by
.= (G * (i,k)) `1 by ;
then A15: LSeg ((G * (i,j)),(G * (i,k))) is vertical by SPPOL_1:16;
j1 <= k by ;
then A16: j1 <= width G by ;
then A17: (G * (i,j)) `2 <= (G * (i,j1)) `2 by ;
A18: k1 <= width G by ;
then A19: (G * (i,j1)) `2 <= (G * (i,k1)) `2 by ;
(G * (i,j1)) `1 = (G * (i,1)) `1 by
.= (G * (i,k1)) `1 by ;
then A20: LSeg ((G * (i,j1)),(G * (i,k1))) is vertical by SPPOL_1:16;
(G * (i,j)) `1 = (G * (i,1)) `1 by
.= (G * (i,j1)) `1 by ;
hence LSeg ((G * (i,j1)),(G * (i,k1))) c= LSeg ((G * (i,j)),(G * (i,k))) by ; :: thesis: verum