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