let G be Go-board; for i, j, k, j1, k1 being Element of 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 Element of NAT ; ( 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
; 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:24;
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:3
.=
(G * i,k) `1
by A1, A2, A7, A12, GOBOARD5:3
;
then A15:
LSeg (G * i,j),(G * i,k) is vertical
by SPPOL_1:37;
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:24;
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:24;
(G * i,j1) `1 =
(G * i,1) `1
by A1, A2, A11, A16, GOBOARD5:3
.=
(G * i,k1) `1
by A1, A2, A9, A18, GOBOARD5:3
;
then A20:
LSeg (G * i,j1),(G * i,k1) is vertical
by SPPOL_1:37;
(G * i,j) `1 =
(G * i,1) `1
by A1, A2, A3, A14, GOBOARD5:3
.=
(G * i,j1) `1
by A1, A2, A11, A16, GOBOARD5:3
;
hence
LSeg (G * i,j1),(G * i,k1) c= LSeg (G * i,j),(G * i,k)
by A15, A20, A17, A19, A10, GOBOARD7:65; verum