let i be Element of NAT ; :: thesis:
let G be Go-board; :: thesis:
assume A1: ( 1 <= i & i < len G & 1 < width G ) ; :: thesis:
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);
A2: i + 1 >= 1 by NAT_1:11;
A3: (0 + 1) + 1 = 0 + (1 + 1) ;
A4: 0 + (1 + 1) <= width G by A1, NAT_1:13;
A5: i + 1 <= len G by A1, NAT_1:13;
then A6: (G * (i + 1),1) `1 = (G * (i + 1),2) `1 by A2, A4, GOBOARD5:3;
A7: (G * (i + 1),1) `2 = (G * 1,(0 + 1)) `2 by A1, A2, A5, GOBOARD5:2
.= (G * i,1) `2 by A1, GOBOARD5:2 ;
then (G * i,1) `2 < (G * (i + 1),2) `2 by A2, A4, A5, GOBOARD5:5;
then ((G * (i + 1),2) `2 ) - ((G * i,1) `2 ) > 0 by XREAL_1:52;
then (1 / 2) * (((G * (i + 1),2) `2 ) - ((G * i,1) `2 )) > 0 by XREAL_1:131;
then A9: 1 < ((1 / 2) * (((G * (i + 1),2) `2 ) - ((G * i,1) `2 ))) + 1 by XREAL_1:31;
then A10: 0 < 1 / (((1 / 2) * (((G * (i + 1),2) `2 ) - ((G * i,1) `2 ))) + 1) ;
A11: 1 / (((1 / 2) * (((G * (i + 1),2) `2 ) - ((G * i,1) `2 ))) + 1) < 1 by A9, XREAL_1:214;
A12: (((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, A9, XCMPLX_1:107 ;
A13: ((((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 ;
((((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 A12, Lm3 ;
then A14: (((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 A13, EUCLID:57
.= (1 / 2) * (G * (i + 1),1) by EUCLID:57 ;
A15: ((((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 ;
(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 A14, 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 A15, 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 A10, A11;
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 A10, A11, TOPREAL1:11;
set I1 = Int (cell G,i,0 );
set I2 = Int (cell G,i,1);
A17: 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, Th49;
A18: 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, A3, Th46;
((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 ;
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, A17, A18, XBOOLE_1:13; :: thesis: