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 A5, A6, XXREAL_0:2;

j <= k1 by A4, A5, XXREAL_0:2;

then A9: 1 <= k1 by A3, XXREAL_0:2;

then A10: (G * (i,k1)) `2 <= (G * (i,k)) `2 by A1, A2, A6, A7, SPRECT_3:12;

A11: 1 <= j1 by A3, A4, XXREAL_0:2;

1 <= j1 by A3, A4, XXREAL_0:2;

then A12: 1 <= k by A8, XXREAL_0:2;

A13: k1 <= width G by A6, A7, XXREAL_0:2;

j <= k1 by A4, A5, XXREAL_0:2;

then A14: j <= width G by A13, XXREAL_0:2;

then (G * (i,j)) `1 = (G * (i,1)) `1 by A1, A2, A3, GOBOARD5:2

.= (G * (i,k)) `1 by A1, A2, A7, A12, GOBOARD5:2 ;

then A15: LSeg ((G * (i,j)),(G * (i,k))) is vertical by SPPOL_1:16;

j1 <= k by A5, A6, XXREAL_0:2;

then A16: j1 <= width G by A7, XXREAL_0:2;

then A17: (G * (i,j)) `2 <= (G * (i,j1)) `2 by A1, A2, A3, A4, SPRECT_3:12;

A18: k1 <= width G by A6, A7, XXREAL_0:2;

then A19: (G * (i,j1)) `2 <= (G * (i,k1)) `2 by A1, A2, A5, A11, SPRECT_3:12;

(G * (i,j1)) `1 = (G * (i,1)) `1 by A1, A2, A11, A16, GOBOARD5:2

.= (G * (i,k1)) `1 by A1, A2, A9, A18, GOBOARD5:2 ;

then A20: LSeg ((G * (i,j1)),(G * (i,k1))) is vertical by SPPOL_1:16;

(G * (i,j)) `1 = (G * (i,1)) `1 by A1, A2, A3, A14, GOBOARD5:2

.= (G * (i,j1)) `1 by A1, A2, A11, A16, GOBOARD5:2 ;

hence LSeg ((G * (i,j1)),(G * (i,k1))) c= LSeg ((G * (i,j)),(G * (i,k))) by A15, A20, A17, A19, A10, GOBOARD7:63; :: thesis: verum

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 A5, A6, XXREAL_0:2;

j <= k1 by A4, A5, XXREAL_0:2;

then A9: 1 <= k1 by A3, XXREAL_0:2;

then A10: (G * (i,k1)) `2 <= (G * (i,k)) `2 by A1, A2, A6, A7, SPRECT_3:12;

A11: 1 <= j1 by A3, A4, XXREAL_0:2;

1 <= j1 by A3, A4, XXREAL_0:2;

then A12: 1 <= k by A8, XXREAL_0:2;

A13: k1 <= width G by A6, A7, XXREAL_0:2;

j <= k1 by A4, A5, XXREAL_0:2;

then A14: j <= width G by A13, XXREAL_0:2;

then (G * (i,j)) `1 = (G * (i,1)) `1 by A1, A2, A3, GOBOARD5:2

.= (G * (i,k)) `1 by A1, A2, A7, A12, GOBOARD5:2 ;

then A15: LSeg ((G * (i,j)),(G * (i,k))) is vertical by SPPOL_1:16;

j1 <= k by A5, A6, XXREAL_0:2;

then A16: j1 <= width G by A7, XXREAL_0:2;

then A17: (G * (i,j)) `2 <= (G * (i,j1)) `2 by A1, A2, A3, A4, SPRECT_3:12;

A18: k1 <= width G by A6, A7, XXREAL_0:2;

then A19: (G * (i,j1)) `2 <= (G * (i,k1)) `2 by A1, A2, A5, A11, SPRECT_3:12;

(G * (i,j1)) `1 = (G * (i,1)) `1 by A1, A2, A11, A16, GOBOARD5:2

.= (G * (i,k1)) `1 by A1, A2, A9, A18, GOBOARD5:2 ;

then A20: LSeg ((G * (i,j1)),(G * (i,k1))) is vertical by SPPOL_1:16;

(G * (i,j)) `1 = (G * (i,1)) `1 by A1, A2, A3, A14, GOBOARD5:2

.= (G * (i,j1)) `1 by A1, A2, A11, A16, GOBOARD5:2 ;

hence LSeg ((G * (i,j1)),(G * (i,k1))) c= LSeg ((G * (i,j)),(G * (i,k))) by A15, A20, A17, A19, A10, GOBOARD7:63; :: thesis: verum