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