let i be Nat; for G being Go-board st 1 <= i & i < len G & 1 < width G holds
LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1)))))) c= ((Int (cell (G,i,((width G) -' 1)))) \/ (Int (cell (G,i,(width G))))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))}
let G be Go-board; ( 1 <= i & i < len G & 1 < width G implies LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1)))))) c= ((Int (cell (G,i,((width G) -' 1)))) \/ (Int (cell (G,i,(width G))))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))} )
assume that
A1:
1 <= i
and
A2:
i < len G
and
A3:
1 < width G
; LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1)))))) c= ((Int (cell (G,i,((width G) -' 1)))) \/ (Int (cell (G,i,(width G))))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))}
set I1 = Int (cell (G,i,((width G) -' 1)));
set I2 = Int (cell (G,i,(width G)));
set p1 = G * (i,(width G));
set q2 = G * ((i + 1),(width G));
set q3 = G * ((i + 1),((width G) -' 1));
set r = 1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1);
A4:
((width G) -' 1) + 1 = width G
by A3, XREAL_1:235;
then A5:
1 <= (width G) -' 1
by A3, NAT_1:13;
A6:
(width G) -' 1 < width G
by A4, NAT_1:13;
then
(G * (i,(width G))) + (G * ((i + 1),((width G) -' 1))) = (G * (i,((width G) -' 1))) + (G * ((i + 1),(width G)))
by A1, A2, A4, A5, Th11;
then A7:
LSeg (((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1)))))) c= (Int (cell (G,i,((width G) -' 1)))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))}
by A1, A2, A4, A5, A6, Th41;
A8:
( i + 1 >= 1 & i + 1 <= len G )
by A2, NAT_1:11, NAT_1:13;
then A9: (G * ((i + 1),(width G))) `1 =
(G * ((i + 1),1)) `1
by A3, GOBOARD5:2
.=
(G * ((i + 1),((width G) -' 1))) `1
by A5, A6, A8, GOBOARD5:2
;
A10: (G * ((i + 1),(width G))) `2 =
(G * (1,(width G))) `2
by A3, A8, GOBOARD5:1
.=
(G * (i,(width G))) `2
by A1, A2, A3, GOBOARD5:1
;
then
(G * ((i + 1),((width G) -' 1))) `2 < (G * (i,(width G))) `2
by A5, A6, A8, GOBOARD5:4;
then A11:
((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2) > 0
by XREAL_1:50;
then
1 < ((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1
by XREAL_1:29, XREAL_1:129;
then A12:
1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1) < 1
by XREAL_1:212;
A13: ((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * |[0,1]|)) `1 =
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) `1) + (((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * |[0,1]|) `1)
by Lm1
.=
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) `1) + (|[((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * 0),((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * 1)]| `1)
by EUCLID:58
.=
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) `1) + 0
by EUCLID:52
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) `1) + (((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1))))) `1)
by Lm1
.=
((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * (((1 / 2) * (G * ((i + 1),(width G)))) `1)) + (((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1))))) `1)
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * (((1 / 2) * (G * ((i + 1),(width G)))) `1)) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * (G * ((i + 1),((width G) -' 1)))) `1))
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * ((G * ((i + 1),(width G))) `1))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * (G * ((i + 1),((width G) -' 1)))) `1))
by Lm3
.=
((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * ((G * ((i + 1),(width G))) `1))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * ((i + 1),(width G))) `1)))
by A9, Lm3
.=
((1 / 2) * (G * ((i + 1),(width G)))) `1
by Lm3
;
A14: ((Int (cell (G,i,((width G) -' 1)))) \/ (Int (cell (G,i,(width G))))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))} =
(Int (cell (G,i,((width G) -' 1)))) \/ ((Int (cell (G,i,(width G)))) \/ ({((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))} \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))}))
by XBOOLE_1:4
.=
(Int (cell (G,i,((width G) -' 1)))) \/ (((Int (cell (G,i,(width G)))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))}) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))})
by XBOOLE_1:4
.=
((Int (cell (G,i,((width G) -' 1)))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))}) \/ ((Int (cell (G,i,(width G)))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))})
by XBOOLE_1:4
;
A15: ((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * (i,(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * (i,(width G)))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G)))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1))))) =
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * (i,(width G))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G)))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * (i,(width G)))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))
by RLVECT_1:def 3
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * (i,(width G))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G)))))) + (((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * (i,(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1))))))
by RLVECT_1:def 3
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * (i,(width G))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G)))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * (G * (i,(width G)))) + ((1 / 2) * (G * ((i + 1),((width G) -' 1))))))
by RLVECT_1:def 5
.=
((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * (((1 / 2) * (G * (i,(width G)))) + ((1 / 2) * (G * ((i + 1),(width G)))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * (G * (i,(width G)))) + ((1 / 2) * (G * ((i + 1),((width G) -' 1))))))
by RLVECT_1:def 5
.=
((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * (((1 / 2) * (G * (i,(width G)))) + ((1 / 2) * (G * ((i + 1),(width G)))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1))))))
by RLVECT_1:def 5
.=
((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1))))))
by RLVECT_1:def 5
;
A16: (((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * ((i + 1),(width G))) `2))) - ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * ((i + 1),((width G) -' 1))) `2)))) + (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) =
(1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * (((G * ((i + 1),(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)
.=
1
by A10, A11, XCMPLX_1:106
;
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * |[0,1]|)) `2 =
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) `2) + (((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * |[0,1]|) `2)
by Lm1
.=
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) `2) + (|[((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * 0),((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * 1)]| `2)
by EUCLID:58
.=
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) `2) + (1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)))
by EUCLID:52
.=
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) `2) + (((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1))))) `2)) + (1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)))
by Lm1
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * (((1 / 2) * (G * ((i + 1),(width G)))) `2)) + (((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1))))) `2)) + (1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * (((1 / 2) * (G * ((i + 1),(width G)))) `2)) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * (G * ((i + 1),((width G) -' 1)))) `2))) + (1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * ((G * ((i + 1),(width G))) `2))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * (((1 / 2) * (G * ((i + 1),((width G) -' 1)))) `2))) + (1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)))
by Lm3
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * ((G * ((i + 1),(width G))) `2))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * ((i + 1),((width G) -' 1))) `2)))) + (1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)))
by Lm3
.=
((1 / 2) * (G * ((i + 1),(width G)))) `2
by A16, Lm3
;
then A17: (((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * |[0,1]|) =
|[(((1 / 2) * (G * ((i + 1),(width G)))) `1),(((1 / 2) * (G * ((i + 1),(width G)))) `2)]|
by A13, EUCLID:53
.=
(1 / 2) * (G * ((i + 1),(width G)))
by EUCLID:53
;
(1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))) =
((1 / 2) * (G * (i,(width G)))) + ((1 / 2) * (G * ((i + 1),(width G))))
by RLVECT_1:def 5
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) + (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * (i,(width G))))) + ((1 / 2) * (G * ((i + 1),(width G))))
by RLVECT_1:def 8
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * (i,(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * (i,(width G)))))) + ((1 / 2) * (G * ((i + 1),(width G))))
by RLVECT_1:def 6
.=
((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * (i,(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * (i,(width G)))))) + (((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1))))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * |[0,1]|)
by A17, RLVECT_1:def 3
.=
(((((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * (i,(width G))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * (i,(width G)))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * (G * ((i + 1),(width G)))))) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * (G * ((i + 1),((width G) -' 1)))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * |[0,1]|)
by RLVECT_1:def 3
.=
(((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) + ((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * |[0,1]|)) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1))))))
by A15, RLVECT_1:def 3
.=
((1 - (1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1))) * (((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|)) + ((1 / (((1 / 2) * (((G * (i,(width G))) `2) - ((G * ((i + 1),((width G) -' 1))) `2))) + 1)) * ((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1))))))
by RLVECT_1:def 5
;
then
(1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))) in LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1))))))
by A11, A12;
then A18:
LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1)))))) = (LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))))) \/ (LSeg (((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1)))))))
by TOPREAL1:5;
LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))) c= (Int (cell (G,i,(width G)))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))}
by A1, A2, Th47;
hence
LSeg ((((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G))))) + |[0,1]|),((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),((width G) -' 1)))))) c= ((Int (cell (G,i,((width G) -' 1)))) \/ (Int (cell (G,i,(width G))))) \/ {((1 / 2) * ((G * (i,(width G))) + (G * ((i + 1),(width G)))))}
by A18, A7, A14, XBOOLE_1:13; verum