let G be Go-board; :: thesis: for i, j, k, j1, k1 being Element of NAT st 1 <= i & i <= width G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg (G * j1,i),(G * k1,i) c= LSeg (G * j,i),(G * k,i)
let i, j, k, j1, k1 be Element of NAT ; :: thesis: ( 1 <= i & i <= width G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G implies LSeg (G * j1,i),(G * k1,i) c= LSeg (G * j,i),(G * k,i) )
assume that
A1: 1 <= i and
A2: i <= width G and
A3: 1 <= j and
A4: j <= j1 and
A5: j1 <= k1 and
A6: k1 <= k and
A7: k <= len G ; :: thesis: LSeg (G * j1,i),(G * k1,i) c= LSeg (G * j,i),(G * k,i)
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 * k1,i) `1 <= (G * k,i) `1 by A1, A2, A6, A7, SPRECT_3:25;
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 <= len G by A6, A7, XXREAL_0:2;
j <= k1 by A4, A5, XXREAL_0:2;
then A14: j <= len G by A13, XXREAL_0:2;
then (G * j,i) `2 = (G * 1,i) `2 by A1, A2, A3, GOBOARD5:2
.= (G * k,i) `2 by A1, A2, A7, A12, GOBOARD5:2 ;
then A15: LSeg (G * j,i),(G * k,i) is horizontal by SPPOL_1:36;
j1 <= k by A5, A6, XXREAL_0:2;
then A16: j1 <= len G by A7, XXREAL_0:2;
then A17: (G * j,i) `1 <= (G * j1,i) `1 by A1, A2, A3, A4, SPRECT_3:25;
A18: k1 <= len G by A6, A7, XXREAL_0:2;
then A19: (G * j1,i) `1 <= (G * k1,i) `1 by A1, A2, A5, A11, SPRECT_3:25;
(G * j1,i) `2 = (G * 1,i) `2 by A1, A2, A11, A16, GOBOARD5:2
.= (G * k1,i) `2 by A1, A2, A9, A18, GOBOARD5:2 ;
then A20: LSeg (G * j1,i),(G * k1,i) is horizontal by SPPOL_1:36;
(G * j,i) `2 = (G * 1,i) `2 by A1, A2, A3, A14, GOBOARD5:2
.= (G * j1,i) `2 by A1, A2, A11, A16, GOBOARD5:2 ;
hence LSeg (G * j1,i),(G * k1,i) c= LSeg (G * j,i),(G * k,i) by A15, A20, A17, A19, A10, GOBOARD7:66; :: thesis: verum