let i, j be Element of NAT ; :: thesis: for G being Go-board st 1 <= i & i <= len G & 1 <= j & j + 2 <= width G holds
(LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2))) = {(G * i,(j + 1))}
let G be Go-board; :: thesis: ( 1 <= i & i <= len G & 1 <= j & j + 2 <= width G implies (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2))) = {(G * i,(j + 1))} )
assume that
A1:
( 1 <= i & i <= len G )
and
A2:
( 1 <= j & j + 2 <= width G )
; :: thesis: (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2))) = {(G * i,(j + 1))}
now let x be
set ;
:: thesis: ( ( x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2))) implies x = G * i,(j + 1) ) & ( x = G * i,(j + 1) implies x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2))) ) )hereby :: thesis: ( x = G * i,(j + 1) implies x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2))) )
assume A3:
x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2)))
;
:: thesis: x = G * i,(j + 1)then A4:
x in LSeg (G * i,j),
(G * i,(j + 1))
by XBOOLE_0:def 4;
reconsider p =
x as
Point of
(TOP-REAL 2) by A3;
j <= j + 2
by NAT_1:11;
then A5:
j <= width G
by A2, XXREAL_0:2;
A6:
j + 1
< j + 2
by XREAL_1:8;
then A7:
( 1
<= j + 1 &
j + 1
<= width G )
by A2, NAT_1:11, XXREAL_0:2;
then (G * i,(j + 1)) `1 =
(G * i,1) `1
by A1, GOBOARD5:3
.=
(G * i,j) `1
by A1, A2, A5, GOBOARD5:3
;
then A8:
p `1 = (G * i,(j + 1)) `1
by A4, Th5;
j < j + 1
by XREAL_1:31;
then
(G * i,j) `2 < (G * i,(j + 1)) `2
by A1, A2, A7, GOBOARD5:5;
then A9:
p `2 <= (G * i,(j + 1)) `2
by A4, TOPREAL1:10;
A10:
(G * i,(j + 1)) `2 < (G * i,(j + 2)) `2
by A1, A2, A6, A7, GOBOARD5:5;
p in LSeg (G * i,(j + 1)),
(G * i,(j + 2))
by A3, XBOOLE_0:def 4;
then
p `2 >= (G * i,(j + 1)) `2
by A10, TOPREAL1:10;
then
p `2 = (G * i,(j + 1)) `2
by A9, XXREAL_0:1;
hence
x = G * i,
(j + 1)
by A8, TOPREAL3:11;
:: thesis: verum
end; assume A11:
x = G * i,
(j + 1)
;
:: thesis: x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2)))then A12:
x in LSeg (G * i,j),
(G * i,(j + 1))
by RLTOPSP1:69;
x in LSeg (G * i,(j + 1)),
(G * i,(j + 2))
by A11, RLTOPSP1:69;
hence
x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2)))
by A12, XBOOLE_0:def 4;
:: thesis: verum end;
hence
(LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2))) = {(G * i,(j + 1))}
by TARSKI:def 1; :: thesis: verum