let G be Go-board; :: thesis: 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 ; :: thesis: ( 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 & i1 + 1 <= len G )
and
A2:
( 1 <= j1 & j1 <= width G )
and
A3:
( 1 <= i2 & i2 + 1 <= len G )
and
A4:
( 1 <= j2 & j2 <= width G )
and
A5:
LSeg (G * i1,j1),(G * (i1 + 1),j1) meets LSeg (G * i2,j2),(G * (i2 + 1),j2)
; :: thesis: ( ( 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)} ) )
A6:
j1 = j2
by A1, A2, A3, A4, A5, Th22;
reconsider m = abs (i1 - i2) as Element of NAT ;
m <= 1
by A1, A2, A3, A4, A5, Th22;
then A7:
( abs (i1 - i2) = 0 or abs (i1 - i2) = 1 )
by NAT_1:26;
A8:
(i1 + 1) + 1 = i1 + (1 + 1)
;
A9:
(i2 + 1) + 1 = i2 + (1 + 1)
;
per cases
( i1 = i2 or i1 = i2 + 1 or i1 + 1 = i2 )
by A7, Th2, GOBOARD1:1;
case
i1 = i2 + 1
;
:: thesis: (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 A1, A2, A3, A6, A9, Th16;
:: thesis: verum end; case
i1 + 1
= i2
;
:: thesis: (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, A2, A3, A6, A8, Th16;
:: thesis: verum end;