let j be Element of 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, Th51, NAT_1:11;
j < j + 1
by XREAL_1:31;
then
(G * 1,j) `2 < (G * 1,(j + 1)) `2
by A1, A2, A3, GOBOARD5:5;
then A9:
((G * 1,(j + 1)) `2 ) - ((G * 1,j) `2 ) > 0
by XREAL_1:52;
A10:
j + 1 >= 1
by NAT_1:11;
then A11: (G * 1,(j + 1)) `1 =
(G * 1,1) `1
by A1, A3, GOBOARD5:3
.=
(G * 1,(j + 2)) `1
by A1, A6, A5, GOBOARD5:3
;
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:3
.=
(G * 1,(j + 1)) `1
by A1, A3, A10, GOBOARD5:3
;
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:8;
then
(G * 1,(j + 1)) `2 < (G * 1,(j + 2)) `2
by A1, A10, A6, GOBOARD5:5;
then A14:
((G * 1,(j + 1)) `2 ) - ((G * 1,j) `2 ) < ((G * 1,(j + 2)) `2 ) - ((G * 1,j) `2 )
by XREAL_1:11;
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:88;
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:57
.=
G * 1,(j + 1)
by EUCLID:57
;
G * 1,(j + 1) =
1 * (G * 1,(j + 1))
by EUCLID:33
.=
((1 / 2) * (G * 1,(j + 1))) + ((1 / 2) * (G * 1,(j + 1)))
by Lm7, EUCLID:37
.=
((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, EUCLID:33
.=
((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 EUCLID:37
.=
(((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 EUCLID:36
.=
(((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 EUCLID:36
.=
((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 EUCLID:30
.=
((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 EUCLID:30
.=
(((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 EUCLID:30
.=
((((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 EUCLID:30
.=
(((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 EUCLID:36
.=
(((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 EUCLID:36
.=
((((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 EUCLID:34
.=
(((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 EUCLID:30
.=
(((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 EUCLID:36
.=
(((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 EUCLID:36
;
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 EUCLID: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 / 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 EUCLID: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))))) + (((((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 EUCLID:34
;
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 EUCLID:53
.=
(((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 EUCLID:53
.=
((((((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 EUCLID:49
.=
(((((((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 EUCLID:49
.=
((((((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 EUCLID:50
.=
((((((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 EUCLID:37
.=
(G * 1,(j + 1)) - |[1,0 ]|
by A16, EUCLID:33
;
(((G * 1,(j + 1)) `2 ) - ((G * 1,j) `2 )) / (((G * 1,(j + 2)) `2 ) - ((G * 1,j) `2 )) < 1
by A14, A9, XREAL_1:191;
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:11;
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, Th52;
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