let i be Element of 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:3;
A7: (G * (i + 1),1) `2 =
(G * 1,(0 + 1)) `2
by A3, A4, GOBOARD5:2
.=
(G * i,1) `2
by A1, A2, A3, GOBOARD5:2
;
then
(G * i,1) `2 < (G * (i + 1),2) `2
by A5, A4, GOBOARD5:5;
then A8:
((G * (i + 1),2) `2 ) - ((G * i,1) `2 ) > 0
by XREAL_1:52;
then
1 < ((1 / 2) * (((G * (i + 1),2) `2 ) - ((G * i,1) `2 ))) + 1
by XREAL_1:31, XREAL_1:131;
then A9:
1 / (((1 / 2) * (((G * (i + 1),2) `2 ) - ((G * i,1) `2 ))) + 1) < 1
by XREAL_1:214;
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, Th49;
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:62
.=
((((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:56
.=
(((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 EUCLID:30
.=
(((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 EUCLID:30
.=
(((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 EUCLID:36
.=
((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 EUCLID:36
.=
((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 EUCLID:36
.=
((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 EUCLID:36
;
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:107
;
((((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:62
.=
((((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:56
.=
((((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:57
.=
(1 / 2) * (G * (i + 1),1)
by EUCLID:57
;
(1 / 2) * ((G * i,1) + (G * (i + 1),1)) =
((1 / 2) * (G * i,1)) + ((1 / 2) * (G * (i + 1),1))
by EUCLID:36
.=
(((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 EUCLID:33
.=
(((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 EUCLID:37
.=
((((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, EUCLID:49
.=
(((((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 EUCLID:30
.=
((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, EUCLID:49
.=
((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 EUCLID:48
.=
((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 EUCLID:45
.=
(((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 EUCLID:51
.=
((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 EUCLID:53
;
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:11;
(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, Th46;
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