let j be Element of NAT ; :: thesis: for G being Go-board st 1 <= j & j < width G & 1 < len G holds
LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))) c= ((Int (cell G,0 ,j)) \/ (Int (cell G,1,j))) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))}
let G be Go-board; :: thesis: ( 1 <= j & j < width G & 1 < len G implies LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))) c= ((Int (cell G,0 ,j)) \/ (Int (cell G,1,j))) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))} )
assume A1:
( 1 <= j & j < width G & 1 < len G )
; :: thesis: LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))) c= ((Int (cell G,0 ,j)) \/ (Int (cell G,1,j))) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))}
set p1 = G * 1,j;
set q2 = G * 1,(j + 1);
set q3 = G * 2,(j + 1);
set r = 1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1);
A2:
j + 1 >= 1
by NAT_1:11;
A3:
(0 + 1) + 1 = 0 + (1 + 1)
;
A4:
0 + (1 + 1) <= len G
by A1, NAT_1:13;
A5:
j + 1 <= width G
by A1, NAT_1:13;
then A6:
(G * 1,(j + 1)) `2 = (G * 2,(j + 1)) `2
by A2, A4, GOBOARD5:2;
A7: (G * 1,(j + 1)) `1 =
(G * 1,1) `1
by A1, A2, A5, GOBOARD5:3
.=
(G * 1,j) `1
by A1, GOBOARD5:3
;
then
(G * 1,j) `1 < (G * 2,(j + 1)) `1
by A2, A4, A5, GOBOARD5:4;
then
((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ) > 0
by XREAL_1:52;
then
(1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 )) > 0
by XREAL_1:131;
then A9:
1 < ((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1
by XREAL_1:31;
then A10:
0 < 1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)
;
A11:
1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1) < 1
by A9, XREAL_1:214;
A12: (((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 2,(j + 1)) `1 ))) - ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,(j + 1)) `1 )))) + (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) =
(1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,(j + 1)) `1 ))) + 1)
.=
1
by A7, A9, XCMPLX_1:107
;
A13: ((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) - ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|)) `2 =
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) `2 ) - (((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|) `2 )
by Lm2
.=
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) `2 ) - (|[((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * 1),((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * 0 )]| `2 )
by EUCLID:62
.=
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) `2 ) - 0
by EUCLID:56
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) `2 ) + (((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1)))) `2 )
by Lm1
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * (((1 / 2) * (G * 1,(j + 1))) `2 )) + (((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1)))) `2 )
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * (((1 / 2) * (G * 1,(j + 1))) `2 )) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * (((1 / 2) * (G * 2,(j + 1))) `2 ))
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,(j + 1)) `2 ))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * (((1 / 2) * (G * 2,(j + 1))) `2 ))
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,(j + 1)) `2 ))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,(j + 1)) `2 )))
by A6, Lm3
.=
((1 / 2) * (G * 1,(j + 1))) `2
by Lm3
;
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) - ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|)) `1 =
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) `1 ) - (((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|) `1 )
by Lm2
.=
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) `1 ) - (|[((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * 1),((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * 0 )]| `1 )
by EUCLID:62
.=
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) `1 ) - (1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)))
by EUCLID:56
.=
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) `1 ) + (((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1)))) `1 )) - (1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)))
by Lm1
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * (((1 / 2) * (G * 1,(j + 1))) `1 )) + (((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1)))) `1 )) - (1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * (((1 / 2) * (G * 1,(j + 1))) `1 )) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * (((1 / 2) * (G * 2,(j + 1))) `1 ))) - (1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,(j + 1)) `1 ))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * (((1 / 2) * (G * 2,(j + 1))) `1 ))) - (1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,(j + 1)) `1 ))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 2,(j + 1)) `1 )))) - (1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)))
by Lm3
.=
((1 / 2) * (G * 1,(j + 1))) `1
by A12, Lm3
;
then A14: (((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) - ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|) =
|[(((1 / 2) * (G * 1,(j + 1))) `1 ),(((1 / 2) * (G * 1,(j + 1))) `2 )]|
by A13, EUCLID:57
.=
(1 / 2) * (G * 1,(j + 1))
by EUCLID:57
;
A15: ((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,j))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 1,j)))) + ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1))))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1)))) =
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,j))) + ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1))))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 1,j)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))
by EUCLID:30
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,j))) + ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1))))) + (((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 1,j))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1)))))
by EUCLID:30
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,j))) + ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1))))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * (((1 / 2) * (G * 1,j)) + ((1 / 2) * (G * 2,(j + 1)))))
by EUCLID:36
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * (((1 / 2) * (G * 1,j)) + ((1 / 2) * (G * 1,(j + 1))))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * (((1 / 2) * (G * 1,j)) + ((1 / 2) * (G * 2,(j + 1)))))
by EUCLID:36
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * (((1 / 2) * (G * 1,j)) + ((1 / 2) * (G * 1,(j + 1))))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))))
by EUCLID:36
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))))
by EUCLID:36
;
(1 / 2) * ((G * 1,j) + (G * 1,(j + 1))) =
((1 / 2) * (G * 1,j)) + ((1 / 2) * (G * 1,(j + 1)))
by EUCLID:36
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) + (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,j))) + ((1 / 2) * (G * 1,(j + 1)))
by EUCLID:33
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,j))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 1,j)))) + ((1 / 2) * (G * 1,(j + 1)))
by EUCLID:37
.=
((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,j))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 1,j)))) + (((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1)))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1)))))) - ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|)
by A14, EUCLID:49
.=
(((((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,j))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 1,j)))) + ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * (G * 1,(j + 1))))) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * (G * 2,(j + 1))))) - ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|)
by EUCLID:30
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))) + (((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,j) + (G * 2,(j + 1))))) - ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|))
by A15, EUCLID:49
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))) + (- (((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|) - ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))))))
by EUCLID:48
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))) - (((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|) - ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,j) + (G * 2,(j + 1))))))
by EUCLID:45
.=
(((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))) - ((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * |[1,0 ]|)) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))))
by EUCLID:51
.=
((1 - (1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1))) * (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|)) + ((1 / (((1 / 2) * (((G * 2,(j + 1)) `1 ) - ((G * 1,j) `1 ))) + 1)) * ((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))))
by EUCLID:53
;
then
(1 / 2) * ((G * 1,j) + (G * 1,(j + 1))) in LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),((1 / 2) * ((G * 1,j) + (G * 2,(j + 1))))
by A10, A11;
then A16:
LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))) = (LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))) \/ (LSeg ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))),((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))))
by A10, A11, TOPREAL1:11;
set I1 = Int (cell G,0 ,j);
set I2 = Int (cell G,1,j);
A17:
LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) c= (Int (cell G,0 ,j)) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))}
by A1, Th47;
A18:
LSeg ((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))),((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))) c= (Int (cell G,1,j)) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))}
by A1, A3, Th43;
((Int (cell G,0 ,j)) \/ (Int (cell G,1,j))) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))} =
(Int (cell G,0 ,j)) \/ ((Int (cell G,1,j)) \/ ({((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))} \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))}))
by XBOOLE_1:4
.=
(Int (cell G,0 ,j)) \/ (((Int (cell G,1,j)) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))}) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))})
by XBOOLE_1:4
.=
((Int (cell G,0 ,j)) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))}) \/ ((Int (cell G,1,j)) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))})
by XBOOLE_1:4
;
hence
LSeg (((1 / 2) * ((G * 1,j) + (G * 1,(j + 1)))) - |[1,0 ]|),((1 / 2) * ((G * 1,j) + (G * 2,(j + 1)))) c= ((Int (cell G,0 ,j)) \/ (Int (cell G,1,j))) \/ {((1 / 2) * ((G * 1,j) + (G * 1,(j + 1))))}
by A16, A17, A18, XBOOLE_1:13; :: thesis: verum