theorem Th24: :: GOBOARD5:24

for 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 + 1 <= width G holds
(h_strip (G,j)) /\ (h_strip (G,(j + 1))) = { q where q is Point of (TOP-REAL 2) : q `2 = (G * (1,(j + 1))) `2 }