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