let G be Go-board; for i1, j1, i2, j2 being Element of NAT st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * (i1 + 1),j1) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) & not ( i1 = i2 & LSeg (G * i1,j1),(G * (i1 + 1),j1) = LSeg (G * i2,j2),(G * (i2 + 1),j2) ) & not ( i1 = i2 + 1 & (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) holds
( i1 + 1 = i2 & (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i2,j2)} )
let i1, j1, i2, j2 be Element of NAT ; ( 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * (i1 + 1),j1) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) & not ( i1 = i2 & LSeg (G * i1,j1),(G * (i1 + 1),j1) = LSeg (G * i2,j2),(G * (i2 + 1),j2) ) & not ( i1 = i2 + 1 & (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) implies ( i1 + 1 = i2 & (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i2,j2)} ) )
assume that
A1:
1 <= i1
and
A2:
i1 + 1 <= len G
and
A3:
( 1 <= j1 & j1 <= width G )
and
A4:
1 <= i2
and
A5:
i2 + 1 <= len G
and
A6:
( 1 <= j2 & j2 <= width G & LSeg (G * i1,j1),(G * (i1 + 1),j1) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) )
; ( ( i1 = i2 & LSeg (G * i1,j1),(G * (i1 + 1),j1) = LSeg (G * i2,j2),(G * (i2 + 1),j2) ) or ( i1 = i2 + 1 & (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)} ) or ( i1 + 1 = i2 & (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i2,j2)} ) )
A7:
j1 = j2
by A1, A2, A3, A4, A5, A6, Th22;
reconsider m = abs (i1 - i2) as Element of NAT ;
A8:
(i1 + 1) + 1 = i1 + (1 + 1)
;
A9:
(i2 + 1) + 1 = i2 + (1 + 1)
;
A10:
( abs (i1 - i2) = 0 or abs (i1 - i2) = 1 )
by A1, A2, A3, A4, A5, A6, Th22, NAT_1:26;
per cases
( i1 = i2 or i1 = i2 + 1 or i1 + 1 = i2 )
by A10, Th2, GOBOARD1:1;
case
i1 = i2
;
LSeg (G * i1,j1),(G * (i1 + 1),j1) = LSeg (G * i2,j2),(G * (i2 + 1),j2)hence
LSeg (G * i1,j1),
(G * (i1 + 1),j1) = LSeg (G * i2,j2),
(G * (i2 + 1),j2)
by A7;
verum end; case
i1 = i2 + 1
;
(LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)}hence
(LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i1,j1)}
by A2, A3, A4, A7, A9, Th16;
verum end; case
i1 + 1
= i2
;
(LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i2,j2)}hence
(LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i2,j2),(G * (i2 + 1),j2)) = {(G * i2,j2)}
by A1, A3, A5, A7, A8, Th16;
verum end;