theorem Th20: :: GOBOARD5:20

for i, j being Nat
for G being Matrix of (TOP-REAL 2) st G is X_equal-in-line & G is X_increasing-in-column & 1 <= j & j <= width G & 1 <= i & i + 1 <= len G holds
LSeg ((G * (i,j)),(G * ((i + 1),j))) c= v_strip (G,i)