let j be 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 that
A1: 1 <= j and
A2: j < width G and
A3: 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);
A4: ( j + 1 >= 1 & j + 1 <= width G ) by A2, NAT_1:11, NAT_1:13;
A5: 0 + (1 + 1) <= len G by A3, NAT_1:13;
then A6: (G * (1,(j + 1))) `2 = (G * (2,(j + 1))) `2 by A4, GOBOARD5:1;
A7: (G * (1,(j + 1))) `1 = (G * (1,1)) `1 by A3, A4, GOBOARD5:2
.= (G * (1,j)) `1 by A1, A2, A3, GOBOARD5:2 ;
then (G * (1,j)) `1 < (G * (2,(j + 1))) `1 by A5, A4, GOBOARD5:3;
then A8: ((G * (2,(j + 1))) `1) - ((G * (1,j)) `1) > 0 by XREAL_1:50;
then 1 < ((1 / 2) * (((G * (2,(j + 1))) `1) - ((G * (1,j)) `1))) + 1 by XREAL_1:29, XREAL_1:129;
then A9: 1 / (((1 / 2) * (((G * (2,(j + 1))) `1) - ((G * (1,j)) `1))) + 1) < 1 by XREAL_1:212;
set I1 = Int (cell (G,0,j));
set I2 = Int (cell (G,1,j));
A10: 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, A2, Th44;
A11: ((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 ;
A12: ((((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:58
.= ((((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:52
.= (((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 ;
A13: ((((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 RLVECT_1:def 3
.= (((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 RLVECT_1:def 3
.= (((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 RLVECT_1:def 5
.= ((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 RLVECT_1:def 5
.= ((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 RLVECT_1:def 5
.= ((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 RLVECT_1:def 5 ;
A14: (((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, A8, XCMPLX_1:106 ;
((((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:58
.= ((((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:52
.= ((((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 A14, Lm3 ;
then A15: (((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 A12, EUCLID:53
.= (1 / 2) * (G * (1,(j + 1))) by EUCLID:53 ;
(1 / 2) * ((G * (1,j)) + (G * (1,(j + 1)))) = ((1 / 2) * (G * (1,j))) + ((1 / 2) * (G * (1,(j + 1)))) by RLVECT_1:def 5
.= (((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 RLVECT_1:def 8
.= (((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 RLVECT_1:def 6
.= ((((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 A15, RLVECT_1:def 3
.= (((((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 RLVECT_1:def 3
.= ((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 A13, RLVECT_1:def 3
.= ((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 RLVECT_1:33
.= ((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)))))))
.= (((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 RLVECT_1:29
.= ((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 RLVECT_1:34 ;
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 A8, A9;
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 TOPREAL1:5;
(0 + 1) + 1 = 0 + (1 + 1) ;
then 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, A2, A3, Th40;
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, A10, A11, XBOOLE_1:13; :: thesis: verum