let i, j be Nat; :: thesis: 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 & 1 <= j & j <= width G & 1 <= i & i < len G holds
LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j)
let G be Matrix of (TOP-REAL 2); :: thesis: ( G is empty-yielding & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G implies LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j) )
assume that
A1: G is empty-yielding and
A2: G is Y_equal-in-column and
A3: G is Y_increasing-in-line and
A4: 1 <= j and
A5: j <= width G and
A6: 1 <= i and
A7: i < len G ; :: thesis: LSeg ((G * (i,j)),(G * ((i + 1),j))) c= h_strip (G,j)
A8: 1 <= i + 1 by A6, NAT_1:13;
A9: i + 1 <= len G by A7, NAT_1:13;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg ((G * (i,j)),(G * ((i + 1),j))) or x in h_strip (G,j) )
assume A10: x in LSeg ((G * (i,j)),(G * ((i + 1),j))) ; :: thesis: x in h_strip (G,j)
then reconsider p = x as Point of (TOP-REAL 2) ;
A11: p = |[(p `1),(p `2)]| by EUCLID:53;
A12: (G * (i,j)) `2 = (G * (1,j)) `2 by A2, A4, A5, A6, A7, Th1
.= (G * ((i + 1),j)) `2 by A2, A4, A5, A8, A9, Th1 ;

now :: thesis: x in h_strip (G,j)

per cases ( j = width G or j < width G ) by A5, XXREAL_0:1;

suppose A13: j = width G ; :: thesis: x in h_strip (G,j)

then (G * (i,(width G))) `2 <= p `2 by A10, A12, TOPREAL1:4;
then p in { |[r,s]| where r, s is Real : (G * (i,(width G))) `2 <= s } by A11;
hence x in h_strip (G,j) by A1, A2, A6, A7, A13, Th6; :: thesis: verum

end;

suppose A14: j < width G ; :: thesis: x in h_strip (G,j)

then A15: j + 1 <= width G by NAT_1:13;
A16: (G * (i,j)) `2 <= p `2 by A10, A12, TOPREAL1:4;
p `2 <= (G * (i,j)) `2 by A10, A12, TOPREAL1:4;
then A17: p `2 = (G * (i,j)) `2 by A16, XXREAL_0:1;
j < j + 1 by XREAL_1:29;
then p `2 < (G * (i,(j + 1))) `2 by A3, A4, A6, A7, A15, A17, Th4;
then p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `2 <= s & s <= (G * (i,(j + 1))) `2 ) } by A11, A16;
hence x in h_strip (G,j) by A2, A4, A6, A7, A14, Th5; :: thesis: verum

end;

end;

end;

hence x in h_strip (G,j) ; :: thesis: verum