let i be 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