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