let i, j be Element of NAT ; for G being Go-board st 1 <= i & i < len G & 1 <= j & j < width G holds
LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))) c= (Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}
let G be Go-board; ( 1 <= i & i < len G & 1 <= j & j < width G implies LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))) c= (Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} )
assume that
A1:
1 <= i
and
A2:
i < len G
and
A3:
1 <= j
and
A4:
j < width G
; LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))) c= (Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}
let x be set ; TARSKI:def 3 ( not x in LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))) or x in (Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))} )
assume A5:
x in LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))
; x in (Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}
then reconsider p = x as Point of (TOP-REAL 2) ;
consider r being Real such that
A6:
p = ((1 - r) * ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1))))) + (r * ((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))))
and
A7:
0 <= r
and
A8:
r <= 1
by A5;
now per cases
( r = 1 or r < 1 )
by A8, XXREAL_0:1;
case A9:
r < 1
;
p in Int (cell G,i,j)set r3 =
(1 - r) * (1 / 2);
set s3 =
r * (1 / 2);
set r1 =
(G * i,1) `1 ;
set r2 =
(G * (i + 1),1) `1 ;
set s1 =
(G * 1,j) `2 ;
set s2 =
(G * 1,(j + 1)) `2 ;
A10:
(((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * i,1) `1 ))) + ((r * (1 / 2)) * (((G * i,1) `1 ) + ((G * i,1) `1 ))) = (G * i,1) `1
;
0 <> width G
by GOBOARD1:def 5;
then A11:
1
<= width G
by NAT_1:14;
A12:
i + 1
<= len G
by A2, NAT_1:13;
i < i + 1
by XREAL_1:31;
then A13:
(G * i,1) `1 < (G * (i + 1),1) `1
by A1, A12, A11, GOBOARD5:4;
then A14:
((G * i,1) `1 ) + ((G * i,1) `1 ) < ((G * i,1) `1 ) + ((G * (i + 1),1) `1 )
by XREAL_1:8;
((G * i,1) `1 ) + ((G * (i + 1),1) `1 ) < ((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 )
by A13, XREAL_1:8;
then
((G * i,1) `1 ) + ((G * i,1) `1 ) < ((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 )
by A14, XXREAL_0:2;
then A15:
(r * (1 / 2)) * (((G * i,1) `1 ) + ((G * i,1) `1 )) <= (r * (1 / 2)) * (((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 ))
by A7, XREAL_1:66;
1
- r > 0
by A9, XREAL_1:52;
then A16:
(1 - r) * (1 / 2) > (1 / 2) * 0
by XREAL_1:70;
then
((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * i,1) `1 )) < ((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * (i + 1),1) `1 ))
by A14, XREAL_1:70;
then A17:
(G * i,1) `1 < (((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * (i + 1),1) `1 ))) + ((r * (1 / 2)) * (((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 )))
by A15, A10, XREAL_1:10;
0 <> len G
by GOBOARD1:def 5;
then A18:
1
<= len G
by NAT_1:14;
A19:
1
<= j + 1
by A3, NAT_1:13;
A20:
Int (cell G,i,j) = { |[r9,s9]| where r9, s9 is Real : ( (G * i,1) `1 < r9 & r9 < (G * (i + 1),1) `1 & (G * 1,j) `2 < s9 & s9 < (G * 1,(j + 1)) `2 ) }
by A1, A2, A3, A4, Th29;
A21:
(((1 - r) * (1 / 2)) * (((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 ))) + ((r * (1 / 2)) * (((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 ))) = (G * 1,(j + 1)) `2
;
A22:
G * i,
j =
|[((G * i,j) `1 ),((G * i,j) `2 )]|
by EUCLID:57
.=
|[((G * i,1) `1 ),((G * i,j) `2 )]|
by A1, A2, A3, A4, GOBOARD5:3
.=
|[((G * i,1) `1 ),((G * 1,j) `2 )]|
by A1, A2, A3, A4, GOBOARD5:2
;
A23:
(((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,j) `2 ))) + ((r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,j) `2 ))) = (G * 1,j) `2
;
A24:
1
<= i + 1
by A1, NAT_1:13;
A25:
G * (i + 1),
j =
|[((G * (i + 1),j) `1 ),((G * (i + 1),j) `2 )]|
by EUCLID:57
.=
|[((G * (i + 1),1) `1 ),((G * (i + 1),j) `2 )]|
by A3, A4, A24, A12, GOBOARD5:3
.=
|[((G * (i + 1),1) `1 ),((G * 1,j) `2 )]|
by A3, A4, A24, A12, GOBOARD5:2
;
A26:
(((1 - r) * (1 / 2)) * (((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 ))) + ((r * (1 / 2)) * (((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 ))) = (G * (i + 1),1) `1
;
((G * i,1) `1 ) + ((G * (i + 1),1) `1 ) < ((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 )
by A13, XREAL_1:8;
then
((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * (i + 1),1) `1 )) < ((1 - r) * (1 / 2)) * (((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 ))
by A16, XREAL_1:70;
then A27:
(((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * (i + 1),1) `1 ))) + ((r * (1 / 2)) * (((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 ))) < (G * (i + 1),1) `1
by A26, XREAL_1:10;
A28:
j + 1
<= width G
by A4, NAT_1:13;
A29:
G * (i + 1),
(j + 1) =
|[((G * (i + 1),(j + 1)) `1 ),((G * (i + 1),(j + 1)) `2 )]|
by EUCLID:57
.=
|[((G * (i + 1),1) `1 ),((G * (i + 1),(j + 1)) `2 )]|
by A19, A28, A24, A12, GOBOARD5:3
.=
|[((G * (i + 1),1) `1 ),((G * 1,(j + 1)) `2 )]|
by A19, A28, A24, A12, GOBOARD5:2
;
j < j + 1
by XREAL_1:31;
then A30:
(G * 1,j) `2 < (G * 1,(j + 1)) `2
by A3, A28, A18, GOBOARD5:5;
then A31:
((G * 1,j) `2 ) + ((G * 1,j) `2 ) < ((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )
by XREAL_1:8;
then A32:
(r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,j) `2 )) <= (r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))
by A7, XREAL_1:66;
((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,j) `2 )) < ((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))
by A16, A31, XREAL_1:70;
then A33:
(G * 1,j) `2 < (((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))) + ((r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )))
by A32, A23, XREAL_1:10;
A34:
((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ) < ((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 )
by A30, XREAL_1:8;
then A35:
(r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )) <= (r * (1 / 2)) * (((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 ))
by A7, XREAL_1:66;
((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )) < ((1 - r) * (1 / 2)) * (((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 ))
by A16, A34, XREAL_1:70;
then A36:
(((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))) + ((r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))) < (G * 1,(j + 1)) `2
by A35, A21, XREAL_1:10;
p =
(((1 - r) * (1 / 2)) * ((G * i,j) + (G * (i + 1),(j + 1)))) + (r * ((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1)))))
by A6, EUCLID:34
.=
(((1 - r) * (1 / 2)) * ((G * i,j) + (G * (i + 1),(j + 1)))) + ((r * (1 / 2)) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))
by EUCLID:34
.=
(((1 - r) * (1 / 2)) * |[(((G * i,1) `1 ) + ((G * (i + 1),1) `1 )),(((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))]|) + ((r * (1 / 2)) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))
by A22, A29, EUCLID:60
.=
(((1 - r) * (1 / 2)) * |[(((G * i,1) `1 ) + ((G * (i + 1),1) `1 )),(((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))]|) + ((r * (1 / 2)) * |[(((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 )),(((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))]|)
by A29, A25, EUCLID:60
.=
|[(((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * (i + 1),1) `1 ))),(((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )))]| + ((r * (1 / 2)) * |[(((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 )),(((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))]|)
by EUCLID:62
.=
|[(((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * (i + 1),1) `1 ))),(((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )))]| + |[((r * (1 / 2)) * (((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 ))),((r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )))]|
by EUCLID:62
.=
|[((((1 - r) * (1 / 2)) * (((G * i,1) `1 ) + ((G * (i + 1),1) `1 ))) + ((r * (1 / 2)) * (((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 )))),((((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))) + ((r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))))]|
by EUCLID:60
;
hence
p in Int (cell G,i,j)
by A17, A27, A33, A36, A20;
verum end;
hence
x in (Int (cell G,i,j)) \/ {((1 / 2) * ((G * (i + 1),j) + (G * (i + 1),(j + 1))))}
by XBOOLE_0:def 3; verum