let j be Nat; :: thesis: for G being Go-board st j <= width G holds
h_strip (G,j) is convex
let G be Go-board; :: thesis: ( j <= width G implies h_strip (G,j) is convex )
assume A1: j <= width G ; :: thesis: h_strip (G,j) is convex
set P = h_strip (G,j);
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def 1 :: thesis: ( 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) ) ; :: thesis: 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; :: thesis: verum