let i be Nat; for G being Go-board st 1 < width G & 1 <= i & i + 1 < len G holds
LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),(((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|)) c= ((Int (cell (G,i,(width G)))) \/ (Int (cell (G,(i + 1),(width G))))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)}
let G be Go-board; ( 1 < width G & 1 <= i & i + 1 < len G implies LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),(((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|)) c= ((Int (cell (G,i,(width G)))) \/ (Int (cell (G,(i + 1),(width G))))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)} )
assume that
A1:
1 < width G
and
A2:
1 <= i
and
A3:
i + 1 < len G
; LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),(((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|)) c= ((Int (cell (G,i,(width G)))) \/ (Int (cell (G,(i + 1),(width G))))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)}
set p1 = G * (i,(width G));
set p2 = G * ((i + 1),(width G));
set q3 = G * ((i + 2),(width G));
set r = (((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1));
A4:
(i + 1) + 1 = i + (1 + 1)
;
then A5:
i + 2 >= 1
by NAT_1:11;
A6:
i + (1 + 1) <= len G
by A3, A4, NAT_1:13;
set I1 = Int (cell (G,i,(width G)));
set I2 = Int (cell (G,(i + 1),(width G)));
A7: ((Int (cell (G,i,(width G)))) \/ (Int (cell (G,(i + 1),(width G))))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)} =
(Int (cell (G,i,(width G)))) \/ ((Int (cell (G,(i + 1),(width G)))) \/ ({((G * ((i + 1),(width G))) + |[0,1]|)} \/ {((G * ((i + 1),(width G))) + |[0,1]|)}))
by XBOOLE_1:4
.=
(Int (cell (G,i,(width G)))) \/ (((Int (cell (G,(i + 1),(width G)))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)}) \/ {((G * ((i + 1),(width G))) + |[0,1]|)})
by XBOOLE_1:4
.=
((Int (cell (G,i,(width G)))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)}) \/ ((Int (cell (G,(i + 1),(width G)))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)})
by XBOOLE_1:4
;
A8:
LSeg ((((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|),((G * ((i + 1),(width G))) + |[0,1]|)) c= (Int (cell (G,(i + 1),(width G)))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)}
by A3, A4, Th54, NAT_1:11;
i < i + 1
by XREAL_1:29;
then
(G * (i,(width G))) `1 < (G * ((i + 1),(width G))) `1
by A1, A2, A3, GOBOARD5:3;
then A9:
((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1) > 0
by XREAL_1:50;
A10:
i + 1 >= 1
by NAT_1:11;
then A11: (G * ((i + 1),(width G))) `2 =
(G * (1,(width G))) `2
by A1, A3, GOBOARD5:1
.=
(G * ((i + 2),(width G))) `2
by A1, A6, A5, GOBOARD5:1
;
i <= i + 1
by NAT_1:11;
then A12:
i < len G
by A3, XXREAL_0:2;
then (G * (i,(width G))) `2 =
(G * (1,(width G))) `2
by A1, A2, GOBOARD5:1
.=
(G * ((i + 1),(width G))) `2
by A1, A3, A10, GOBOARD5:1
;
then A13: 1 * ((G * ((i + 1),(width G))) `2) =
((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((G * (i,(width G))) `2)) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((G * ((i + 2),(width G))) `2))
by A11
.=
(((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) `2) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((G * ((i + 2),(width G))) `2))
by Lm3
.=
(((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) `2) + ((((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))) `2)
by Lm3
.=
(((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))) `2
by Lm1
;
i + 1 < i + 2
by XREAL_1:6;
then
(G * ((i + 1),(width G))) `1 < (G * ((i + 2),(width G))) `1
by A1, A10, A6, GOBOARD5:3;
then A14:
((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1) < ((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)
by XREAL_1:9;
then
((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)) = ((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)
by A9, XCMPLX_1:87;
then
(G * ((i + 1),(width G))) `1 = ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((G * (i,(width G))) `1)) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((G * ((i + 2),(width G))) `1))
;
then 1 * ((G * ((i + 1),(width G))) `1) =
(((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) `1) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((G * ((i + 2),(width G))) `1))
by Lm3
.=
(((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) `1) + ((((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))) `1)
by Lm3
.=
(((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))) `1
by Lm1
;
then A15: ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))) =
|[((G * ((i + 1),(width G))) `1),((G * ((i + 1),(width G))) `2)]|
by A13, EUCLID:53
.=
G * ((i + 1),(width G))
by EUCLID:53
;
G * ((i + 1),(width G)) =
1 * (G * ((i + 1),(width G)))
by RLVECT_1:def 8
.=
((1 / 2) * (G * ((i + 1),(width G)))) + ((1 / 2) * (G * ((i + 1),(width G))))
by Lm7, RLVECT_1:def 6
.=
((1 / 2) * (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) + ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G))))) + ((1 / 2) * (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))))
by A15, RLVECT_1:def 8
.=
((1 / 2) * (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G)))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G)))))) + ((1 / 2) * (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))))
by RLVECT_1:def 6
.=
(((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G)))))) + ((1 / 2) * (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))))
by RLVECT_1:def 5
.=
(((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G)))))) + (((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))))
by RLVECT_1:def 5
.=
((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G))))) + (((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G))))) + (((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))))))
by RLVECT_1:def 3
.=
((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G))))) + (((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G))))) + (((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))))))
by RLVECT_1:def 3
.=
(((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G))))) + ((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))))) + (((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))))
by RLVECT_1:def 3
.=
((((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G))))) + ((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G)))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))))
by RLVECT_1:def 3
.=
(((1 / 2) * (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * ((i + 1),(width G)))) + ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (G * (i,(width G)))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G)))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))))
by RLVECT_1:def 5
.=
(((1 / 2) * ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G)))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))))
by RLVECT_1:def 5
.=
((((1 / 2) * (1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))))) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G)))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G)))))
by RLVECT_1:def 7
;
then A16: G * ((i + 1),(width G)) =
(((1 / 2) * (1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))))) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + (((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))))
by RLVECT_1:def 3
.=
(((1 / 2) * (1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))))) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + ((1 / 2) * ((((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 1),(width G)))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (G * ((i + 2),(width G))))))
by RLVECT_1:def 5
.=
(((1 / 2) * (1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))))) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))))
by RLVECT_1:def 5
.=
((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + ((1 / 2) * (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))))
by RLVECT_1:def 7
.=
((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + (((1 / 2) * ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G)))))
by RLVECT_1:def 7
.=
((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))))
by RLVECT_1:def 7
;
A17: ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * (((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|)) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|)) =
(((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * |[0,1]|)) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * (((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|))
by RLVECT_1:def 5
.=
(((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * |[0,1]|)) + ((((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G)))))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * |[0,1]|))
by RLVECT_1:def 5
.=
((((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G)))))) + (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * |[0,1]|))) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * |[0,1]|)
by RLVECT_1:def 3
.=
(((((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G)))))) + ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))))) + ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * |[0,1]|)) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * |[0,1]|)
by RLVECT_1:def 3
.=
((((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G)))))) + ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))))) + (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * |[0,1]|) + (((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * |[0,1]|))
by RLVECT_1:def 3
.=
((((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1))) * ((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G)))))) + ((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))))) + (((1 - ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) + ((((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)))) * |[0,1]|)
by RLVECT_1:def 6
.=
(G * ((i + 1),(width G))) + |[0,1]|
by A16, RLVECT_1:def 8
;
(((G * ((i + 1),(width G))) `1) - ((G * (i,(width G))) `1)) / (((G * ((i + 2),(width G))) `1) - ((G * (i,(width G))) `1)) < 1
by A14, A9, XREAL_1:189;
then
(G * ((i + 1),(width G))) + |[0,1]| in LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),(((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|))
by A14, A9, A17;
then A18:
LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),(((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|)) = (LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((G * ((i + 1),(width G))) + |[0,1]|))) \/ (LSeg (((G * ((i + 1),(width G))) + |[0,1]|),(((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|)))
by TOPREAL1:5;
LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((G * ((i + 1),(width G))) + |[0,1]|)) c= (Int (cell (G,i,(width G)))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)}
by A2, A12, Th55;
hence
LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),(((1 / 2) * ((G * ((i + 1),(width G))) + (G * ((i + 2),(width G))))) + |[0,1]|)) c= ((Int (cell (G,i,(width G)))) \/ (Int (cell (G,(i + 1),(width G))))) \/ {((G * ((i + 1),(width G))) + |[0,1]|)}
by A18, A8, A7, XBOOLE_1:13; verum