let i, j be Element of NAT ; 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; ( 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
and
A3:
j + 2 <= width G
; (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 ;
( ( 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 ( 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 A4:
x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2)))
;
x = G * i,(j + 1)then reconsider p =
x as
Point of
(TOP-REAL 2) ;
A5:
x in LSeg (G * i,j),
(G * i,(j + 1))
by A4, XBOOLE_0:def 4;
A6:
p in LSeg (G * i,(j + 1)),
(G * i,(j + 2))
by A4, XBOOLE_0:def 4;
j <= j + 2
by NAT_1:11;
then A7:
j <= width G
by A3, XXREAL_0:2;
A8:
j + 1
< j + 2
by XREAL_1:8;
then A9:
j + 1
<= width G
by A3, XXREAL_0:2;
A10:
1
<= j + 1
by NAT_1:11;
then (G * i,(j + 1)) `1 =
(G * i,1) `1
by A1, A9, GOBOARD5:3
.=
(G * i,j) `1
by A1, A2, A7, GOBOARD5:3
;
then A11:
p `1 = (G * i,(j + 1)) `1
by A5, Th5;
j < j + 1
by XREAL_1:31;
then
(G * i,j) `2 < (G * i,(j + 1)) `2
by A1, A2, A9, GOBOARD5:5;
then A12:
p `2 <= (G * i,(j + 1)) `2
by A5, TOPREAL1:10;
(G * i,(j + 1)) `2 < (G * i,(j + 2)) `2
by A1, A3, A8, A10, GOBOARD5:5;
then
p `2 >= (G * i,(j + 1)) `2
by A6, TOPREAL1:10;
then
p `2 = (G * i,(j + 1)) `2
by A12, XXREAL_0:1;
hence
x = G * i,
(j + 1)
by A11, TOPREAL3:11;
verum
end; assume
x = G * i,
(j + 1)
;
x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2)))then
(
x in LSeg (G * i,j),
(G * i,(j + 1)) &
x in LSeg (G * i,(j + 1)),
(G * i,(j + 2)) )
by RLTOPSP1:69;
hence
x in (LSeg (G * i,j),(G * i,(j + 1))) /\ (LSeg (G * i,(j + 1)),(G * i,(j + 2)))
by XBOOLE_0:def 4;
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; verum