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