let j be Element of 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