theorem Th23: :: GOBOARD5:23

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