theorem Th15: :: GOBOARD5:15

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