let G be Go-board; for i1, j1, i2, j2 being 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 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, Th19;
A9:
(j1 + 1) + 1 = j1 + (1 + 1)
;
A10:
(j2 + 1) + 1 = j2 + (1 + 1)
;
A11:
( |.(j1 - j2).| = 0 or |.(j1 - j2).| = 1 )
by A1, A2, A3, A4, A5, A6, A7, Th19, NAT_1:25;
per cases
( j1 = j2 or j1 = j2 + 1 or j1 + 1 = j2 )
by A11, Th2, SEQM_3:41;
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, Th13;
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, Th13;
verum end;