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,j) + (G * (i + 1),j))) c= (Int (cell G,i,j)) \/ {((1 / 2) * ((G * i,j) + (G * (i + 1),j)))}
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,j) + (G * (i + 1),j))) c= (Int (cell G,i,j)) \/ {((1 / 2) * ((G * i,j) + (G * (i + 1),j)))} )
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,j) + (G * (i + 1),j))) c= (Int (cell G,i,j)) \/ {((1 / 2) * ((G * i,j) + (G * (i + 1),j)))}
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,j) + (G * (i + 1),j))) or x in (Int (cell G,i,j)) \/ {((1 / 2) * ((G * i,j) + (G * (i + 1),j)))} )
assume A5:
x in LSeg ((1 / 2) * ((G * i,j) + (G * (i + 1),(j + 1)))),((1 / 2) * ((G * i,j) + (G * (i + 1),j)))
; x in (Int (cell G,i,j)) \/ {((1 / 2) * ((G * i,j) + (G * (i + 1),j)))}
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,j) + (G * (i + 1),j))))
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;
then A15:
(r * (1 / 2)) * (((G * i,1) `1 ) + ((G * i,1) `1 )) <= (r * (1 / 2)) * (((G * i,1) `1 ) + ((G * (i + 1),1) `1 ))
by A7, XREAL_1:66;
((G * i,1) `1 ) + ((G * (i + 1),1) `1 ) < ((G * (i + 1),1) `1 ) + ((G * (i + 1),1) `1 )
by A13, XREAL_1:10;
then A16:
(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 A7, XREAL_1:66;
A17:
1
<= i + 1
by A1, NAT_1:13;
1
- r > 0
by A9, XREAL_1:52;
then A18:
(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 A19:
(G * i,1) `1 < (((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 A15, A10, XREAL_1:10;
((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 A20:
((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 A18, XREAL_1:70;
(((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
;
then A21:
(((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 ))) < (G * (i + 1),1) `1
by A20, A16, XREAL_1:10;
A22:
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;
A23:
j + 1
<= width G
by A4, NAT_1:13;
A24:
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, A17, A12, GOBOARD5:3
.=
|[((G * (i + 1),1) `1 ),((G * 1,j) `2 )]|
by A3, A4, A17, A12, GOBOARD5:2
;
A25:
1
<= j + 1
by A3, NAT_1:13;
0 <> len G
by GOBOARD1:def 5;
then A26:
1
<= len G
by NAT_1:14;
A27:
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
;
j < j + 1
by XREAL_1:31;
then A28:
(G * 1,j) `2 < (G * 1,(j + 1)) `2
by A3, A23, A26, GOBOARD5:5;
then
((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ) < ((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 )
by XREAL_1:8;
then A29:
((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 A18, XREAL_1:70;
A30:
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 A25, A23, A17, A12, GOBOARD5:3
.=
|[((G * (i + 1),1) `1 ),((G * 1,(j + 1)) `2 )]|
by A25, A23, A17, A12, GOBOARD5:2
;
A31:
(((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
;
A32:
((G * 1,j) `2 ) + ((G * 1,j) `2 ) < ((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 )
by A28, XREAL_1:8;
then
((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 A18, 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) `2 )))
by A31, XREAL_1:10;
((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ) < ((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 )
by A28, XREAL_1:8;
then
((G * 1,j) `2 ) + ((G * 1,j) `2 ) < ((G * 1,(j + 1)) `2 ) + ((G * 1,(j + 1)) `2 )
by A32, XXREAL_0:2;
then A34:
(r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,j) `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 + 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
;
then A35:
(((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))) + ((r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,j) `2 ))) < (G * 1,(j + 1)) `2
by A29, A34, XREAL_1:10;
p =
(((1 - r) * (1 / 2)) * ((G * i,j) + (G * (i + 1),(j + 1)))) + (r * ((1 / 2) * ((G * i,j) + (G * (i + 1),j))))
by A6, EUCLID:34
.=
(((1 - r) * (1 / 2)) * ((G * i,j) + (G * (i + 1),(j + 1)))) + ((r * (1 / 2)) * ((G * i,j) + (G * (i + 1),j)))
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,j) + (G * (i + 1),j)))
by A27, A30, 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 ) + ((G * (i + 1),1) `1 )),(((G * 1,j) `2 ) + ((G * 1,j) `2 ))]|)
by A27, A24, 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 ) + ((G * (i + 1),1) `1 )),(((G * 1,j) `2 ) + ((G * 1,j) `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 ) + ((G * (i + 1),1) `1 ))),((r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,j) `2 )))]|
by EUCLID:62
.=
|[((((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 )))),((((1 - r) * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,(j + 1)) `2 ))) + ((r * (1 / 2)) * (((G * 1,j) `2 ) + ((G * 1,j) `2 ))))]|
by EUCLID:60
;
hence
p in Int (cell G,i,j)
by A19, A21, A33, A35, A22;
verum end;
hence
x in (Int (cell G,i,j)) \/ {((1 / 2) * ((G * i,j) + (G * (i + 1),j)))}
by XBOOLE_0:def 3; verum