let i be Element of NAT ; for G being Go-board st 1 < width G & 1 <= i & i + 1 < len G holds
LSeg (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|),(((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|) c= ((Int (cell G,i,0 )) \/ (Int (cell G,(i + 1),0 ))) \/ {((G * (i + 1),1) - |[0 ,1]|)}
let G be Go-board; ( 1 < width G & 1 <= i & i + 1 < len G implies LSeg (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|),(((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|) c= ((Int (cell G,i,0 )) \/ (Int (cell G,(i + 1),0 ))) \/ {((G * (i + 1),1) - |[0 ,1]|)} )
assume that
A1:
1 < width G
and
A2:
1 <= i
and
A3:
i + 1 < len G
; LSeg (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|),(((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|) c= ((Int (cell G,i,0 )) \/ (Int (cell G,(i + 1),0 ))) \/ {((G * (i + 1),1) - |[0 ,1]|)}
set p1 = G * i,1;
set p2 = G * (i + 1),1;
set q3 = G * (i + 2),1;
set r = (((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `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,0 );
set I2 = Int (cell G,(i + 1),0 );
A7: ((Int (cell G,i,0 )) \/ (Int (cell G,(i + 1),0 ))) \/ {((G * (i + 1),1) - |[0 ,1]|)} =
(Int (cell G,i,0 )) \/ ((Int (cell G,(i + 1),0 )) \/ ({((G * (i + 1),1) - |[0 ,1]|)} \/ {((G * (i + 1),1) - |[0 ,1]|)}))
by XBOOLE_1:4
.=
(Int (cell G,i,0 )) \/ (((Int (cell G,(i + 1),0 )) \/ {((G * (i + 1),1) - |[0 ,1]|)}) \/ {((G * (i + 1),1) - |[0 ,1]|)})
by XBOOLE_1:4
.=
((Int (cell G,i,0 )) \/ {((G * (i + 1),1) - |[0 ,1]|)}) \/ ((Int (cell G,(i + 1),0 )) \/ {((G * (i + 1),1) - |[0 ,1]|)})
by XBOOLE_1:4
;
A8:
LSeg (((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|),((G * (i + 1),1) - |[0 ,1]|) c= (Int (cell G,(i + 1),0 )) \/ {((G * (i + 1),1) - |[0 ,1]|)}
by A3, A4, Th55, NAT_1:11;
i < i + 1
by XREAL_1:31;
then
(G * i,1) `1 < (G * (i + 1),1) `1
by A1, A2, A3, GOBOARD5:4;
then A9:
((G * (i + 1),1) `1 ) - ((G * i,1) `1 ) > 0
by XREAL_1:52;
A10:
i + 1 >= 1
by NAT_1:11;
then A11: (G * (i + 1),1) `2 =
(G * 1,1) `2
by A1, A3, GOBOARD5:2
.=
(G * (i + 2),1) `2
by A1, A6, A5, GOBOARD5:2
;
i <= i + 1
by NAT_1:11;
then A12:
i < len G
by A3, XXREAL_0:2;
then (G * i,1) `2 =
(G * 1,1) `2
by A1, A2, GOBOARD5:2
.=
(G * (i + 1),1) `2
by A1, A3, A10, GOBOARD5:2
;
then A13: 1 * ((G * (i + 1),1) `2 ) =
((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((G * i,1) `2 )) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((G * (i + 2),1) `2 ))
by A11
.=
(((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) `2 ) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((G * (i + 2),1) `2 ))
by Lm3
.=
(((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) `2 ) + ((((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)) `2 )
by Lm3
.=
(((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))) `2
by Lm1
;
i + 1 < i + 2
by XREAL_1:8;
then
(G * (i + 1),1) `1 < (G * (i + 2),1) `1
by A1, A10, A6, GOBOARD5:4;
then A14:
((G * (i + 1),1) `1 ) - ((G * i,1) `1 ) < ((G * (i + 2),1) `1 ) - ((G * i,1) `1 )
by XREAL_1:11;
then
((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )) = ((G * (i + 1),1) `1 ) - ((G * i,1) `1 )
by A9, XCMPLX_1:88;
then
(G * (i + 1),1) `1 = ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((G * i,1) `1 )) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((G * (i + 2),1) `1 ))
;
then 1 * ((G * (i + 1),1) `1 ) =
(((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) `1 ) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((G * (i + 2),1) `1 ))
by Lm3
.=
(((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) `1 ) + ((((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)) `1 )
by Lm3
.=
(((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))) `1
by Lm1
;
then A15: ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)) =
|[((G * (i + 1),1) `1 ),((G * (i + 1),1) `2 )]|
by A13, EUCLID:57
.=
G * (i + 1),1
by EUCLID:57
;
G * (i + 1),1 =
1 * (G * (i + 1),1)
by EUCLID:33
.=
((1 / 2) * (G * (i + 1),1)) + ((1 / 2) * (G * (i + 1),1))
by Lm7, EUCLID:37
.=
((1 / 2) * (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) + ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1))) + ((1 / 2) * (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))))
by A15, EUCLID:33
.=
((1 / 2) * (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1)))) + ((1 / 2) * (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))))
by EUCLID:37
.=
(((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1)))) + ((1 / 2) * (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))))
by EUCLID:36
.=
(((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1)))) + (((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))))
by EUCLID:36
.=
((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1))) + (((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1))) + (((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)))))
by EUCLID:30
.=
((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1))) + (((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1))) + (((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)))))
by EUCLID:30
.=
(((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1))) + ((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)))) + (((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))))
by EUCLID:30
.=
((((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1))) + ((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1)))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)))
by EUCLID:30
.=
(((1 / 2) * (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * (i + 1),1)) + ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (G * i,1)))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1)))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)))
by EUCLID:36
.=
(((1 / 2) * ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((G * i,1) + (G * (i + 1),1)))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1)))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)))
by EUCLID:36
.=
((((1 / 2) * (1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))))) * ((G * i,1) + (G * (i + 1),1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1)))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1)))
by EUCLID:34
.=
(((1 / 2) * (1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))))) * ((G * i,1) + (G * (i + 1),1))) + (((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))))
by EUCLID:30
.=
(((1 / 2) * (1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))))) * ((G * i,1) + (G * (i + 1),1))) + ((1 / 2) * ((((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 1),1)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (G * (i + 2),1))))
by EUCLID:36
;
then A16: G * (i + 1),1 =
(((1 / 2) * (1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))))) * ((G * i,1) + (G * (i + 1),1))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((G * (i + 1),1) + (G * (i + 2),1))))
by EUCLID:36
.=
((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1)))) + ((1 / 2) * (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((G * (i + 1),1) + (G * (i + 2),1))))
by EUCLID:34
.=
((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1)))) + (((1 / 2) * ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((G * (i + 1),1) + (G * (i + 2),1)))
by EUCLID:34
.=
((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1)))) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))))
by EUCLID:34
;
A17: ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|)) =
(((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1)))) - ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * |[0 ,1]|)) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * (((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|))
by EUCLID:53
.=
(((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1)))) - ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * |[0 ,1]|)) + ((((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1)))) - (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * |[0 ,1]|))
by EUCLID:53
.=
((((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1)))) + (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1)))) - ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * |[0 ,1]|))) - (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * |[0 ,1]|)
by EUCLID:49
.=
(((((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1)))) + ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1))))) - ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * |[0 ,1]|)) - (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * |[0 ,1]|)
by EUCLID:49
.=
((((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1)))) + ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1))))) - (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * |[0 ,1]|) + (((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * |[0 ,1]|))
by EUCLID:50
.=
((((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 ))) * ((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1)))) + ((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * ((1 / 2) * ((G * i,1) + (G * (i + 1),1))))) - (((1 - ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) + ((((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )))) * |[0 ,1]|)
by EUCLID:37
.=
(G * (i + 1),1) - |[0 ,1]|
by A16, EUCLID:33
;
(((G * (i + 1),1) `1 ) - ((G * i,1) `1 )) / (((G * (i + 2),1) `1 ) - ((G * i,1) `1 )) < 1
by A14, A9, XREAL_1:191;
then
(G * (i + 1),1) - |[0 ,1]| in LSeg (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|),(((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|)
by A14, A9, A17;
then A18:
LSeg (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|),(((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|) = (LSeg (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|),((G * (i + 1),1) - |[0 ,1]|)) \/ (LSeg ((G * (i + 1),1) - |[0 ,1]|),(((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|))
by TOPREAL1:11;
LSeg (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|),((G * (i + 1),1) - |[0 ,1]|) c= (Int (cell G,i,0 )) \/ {((G * (i + 1),1) - |[0 ,1]|)}
by A2, A12, Th56;
hence
LSeg (((1 / 2) * ((G * i,1) + (G * (i + 1),1))) - |[0 ,1]|),(((1 / 2) * ((G * (i + 1),1) + (G * (i + 2),1))) - |[0 ,1]|) c= ((Int (cell G,i,0 )) \/ (Int (cell G,(i + 1),0 ))) \/ {((G * (i + 1),1) - |[0 ,1]|)}
by A18, A8, A7, XBOOLE_1:13; verum