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

now

per cases ( j = 0 or j > 0 ) by NAT_1:3;

suppose A14: j = 0 ; :: thesis: x in h_strip G,j

then p `2 <= (G * i,1) `2 by A9, A13, TOPREAL1:10;
then p in { |[r,s]| where r, s is Real : s <= (G * i,1) `2 } by A10;
hence x in h_strip G,j by A1, A2, A5, A6, A14, Th8; :: thesis: verum

end;

suppose j > 0 ; :: thesis: x in h_strip G,j

then A15: 0 + 1 <= j by NAT_1:13;
A16: (G * i,(j + 1)) `2 <= p `2 by A9, A13, TOPREAL1:10;
A17: p `2 <= (G * i,(j + 1)) `2 by A9, A13, TOPREAL1:10;
then A18: p `2 = (G * i,(j + 1)) `2 by A16, XXREAL_0:1;
j < j + 1 by XREAL_1:31;
then (G * i,j) `2 < p `2 by A3, A5, A6, A12, A15, A18, Th5;
then p in { |[r,s]| where r, s is Real : ( (G * i,j) `2 <= s & s <= (G * i,(j + 1)) `2 ) } by A10, A17;
hence x in h_strip G,j by A2, A4, A5, A6, A15, Th6; :: thesis: verum

end;

end;

end;

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