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