let j be Nat; for G being Go-board st j <= width G holds
h_strip (G,j) is convex
let G be Go-board; ( j <= width G implies h_strip (G,j) is convex )
assume A1:
j <= width G
; h_strip (G,j) is convex
set P = h_strip (G,j);
let w1, w2 be Point of (TOP-REAL 2); JORDAN1:def 1 ( not w1 in h_strip (G,j) or not w2 in h_strip (G,j) or LSeg (w1,w2) c= h_strip (G,j) )
assume A2:
( w1 in h_strip (G,j) & w2 in h_strip (G,j) )
; LSeg (w1,w2) c= h_strip (G,j)
( w1 `2 <= w2 `2 or w2 `2 <= w1 `2 )
;
hence
LSeg (w1,w2) c= h_strip (G,j)
by A1, A2, Lm4; verum