let i, j be Nat; for G being Go-board st i < len G & 1 <= j & j < width G holds
(cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))
let G be Go-board; ( i < len G & 1 <= j & j < width G implies (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) )
assume that
A1:
i < len G
and
A2:
1 <= j
and
A3:
j < width G
; (cell (G,i,j)) /\ (cell (G,(i + 1),j)) = LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))
A4:
0 + 1 <= i + 1
by XREAL_1:6;
A5:
i + 1 <= len G
by A1, NAT_1:13;
thus
(cell (G,i,j)) /\ (cell (G,(i + 1),j)) c= LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))
XBOOLE_0:def 10 LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,(i + 1),j))proof
let x be
object ;
TARSKI:def 3 ( not x in (cell (G,i,j)) /\ (cell (G,(i + 1),j)) or x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) )
A6:
(cell (G,i,j)) /\ (cell (G,(i + 1),j)) =
(v_strip (G,i)) /\ (((v_strip (G,(i + 1))) /\ (h_strip (G,j))) /\ (h_strip (G,j)))
by XBOOLE_1:16
.=
(v_strip (G,i)) /\ ((v_strip (G,(i + 1))) /\ ((h_strip (G,j)) /\ (h_strip (G,j))))
by XBOOLE_1:16
.=
((v_strip (G,i)) /\ (v_strip (G,(i + 1)))) /\ (h_strip (G,j))
by XBOOLE_1:16
;
assume A7:
x in (cell (G,i,j)) /\ (cell (G,(i + 1),j))
;
x in LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))
then A8:
x in (v_strip (G,i)) /\ (v_strip (G,(i + 1)))
by A6, XBOOLE_0:def 4;
A9:
x in h_strip (
G,
j)
by A6, A7, XBOOLE_0:def 4;
A10:
j < j + 1
by NAT_1:13;
A11:
j + 1
<= width G
by A3, NAT_1:13;
then A12:
(G * ((i + 1),j)) `2 < (G * ((i + 1),(j + 1))) `2
by A2, A4, A5, A10, Th4;
A13:
G * (
(i + 1),
j)
= |[((G * ((i + 1),j)) `1),((G * ((i + 1),j)) `2)]|
by EUCLID:53;
A14:
j + 1
>= 1
by NAT_1:11;
(G * ((i + 1),j)) `1 =
(G * ((i + 1),1)) `1
by A2, A3, A4, A5, Th2
.=
(G * ((i + 1),(j + 1))) `1
by A4, A5, A11, A14, Th2
;
then A15:
G * (
(i + 1),
(j + 1))
= |[((G * ((i + 1),j)) `1),((G * ((i + 1),(j + 1))) `2)]|
by EUCLID:53;
reconsider p =
x as
Point of
(TOP-REAL 2) by A7;
i + 1
<= len G
by A1, NAT_1:13;
then
p in { q where q is Point of (TOP-REAL 2) : q `1 = (G * ((i + 1),1)) `1 }
by A8, Th23;
then
ex
q being
Point of
(TOP-REAL 2) st
(
q = p &
q `1 = (G * ((i + 1),1)) `1 )
;
then A16:
p `1 = (G * ((i + 1),j)) `1
by A2, A3, A4, A5, Th2;
p in { |[r,s]| where r, s is Real : ( (G * ((i + 1),j)) `2 <= s & s <= (G * ((i + 1),(j + 1))) `2 ) }
by A2, A3, A4, A5, A9, Th5;
then A17:
ex
r,
s being
Real st
(
p = |[r,s]| &
(G * ((i + 1),j)) `2 <= s &
s <= (G * ((i + 1),(j + 1))) `2 )
;
then A18:
(G * ((i + 1),j)) `2 <= p `2
by EUCLID:52;
p `2 <= (G * ((i + 1),(j + 1))) `2
by A17, EUCLID:52;
then
p in { q where q is Point of (TOP-REAL 2) : ( q `1 = (G * ((i + 1),j)) `1 & (G * ((i + 1),j)) `2 <= q `2 & q `2 <= (G * ((i + 1),(j + 1))) `2 ) }
by A16, A18;
hence
x in LSeg (
(G * ((i + 1),j)),
(G * ((i + 1),(j + 1))))
by A12, A13, A15, TOPREAL3:9;
verum
end;
A19:
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j)
by A1, A2, A3, Th18;
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,(i + 1),j)
by A2, A3, A4, A5, Th19;
hence
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= (cell (G,i,j)) /\ (cell (G,(i + 1),j))
by A19, XBOOLE_1:19; verum