let i be Element of NAT ; :: thesis: for G being Go-board st i <= len G holds
v_strip G,i is convex
let G be Go-board; :: thesis: ( i <= len G implies v_strip G,i is convex )
assume A1: i <= len G ; :: thesis: v_strip G,i is convex
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def 1 :: thesis: ( not w1 in v_strip G,i or not w2 in v_strip G,i or LSeg w1,w2 c= v_strip G,i )
set P = v_strip G,i;
A2: ( w1 `1 <= w2 `1 or w2 `1 <= w1 `1 ) ;
assume ( w1 in v_strip G,i & w2 in v_strip G,i ) ; :: thesis: LSeg w1,w2 c= v_strip G,i
hence LSeg w1,w2 c= v_strip G,i by A1, A2, Lm3; :: thesis: verum