theorem Th13: :: GOBOARD5:13

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