let i, j be Element of NAT ; :: thesis: for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G holds
LSeg (G * i,j),(G * i,(j + 1)) c= h_strip G,j
let G be Matrix of (TOP-REAL 2); :: thesis: ( G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= i & i <= len G & 1 <= j & j + 1 <= width G implies LSeg (G * i,j),(G * i,(j + 1)) c= h_strip G,j )
assume that
A1: G is Y_equal-in-column and
A2: G is Y_increasing-in-line and
A3: ( 1 <= i & i <= len G ) and
A4: ( 1 <= j & j + 1 <= width G ) ; :: thesis: LSeg (G * i,j),(G * i,(j + 1)) c= h_strip G,j
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (G * i,j),(G * i,(j + 1)) or x in h_strip G,j )
assume A5: x in LSeg (G * i,j),(G * i,(j + 1)) ; :: thesis: x in h_strip G,j
then reconsider p = x as Point of (TOP-REAL 2) ;
A6: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A7: j < width G by A4, NAT_1:13;
j < j + 1 by XREAL_1:31;
then (G * i,j) `2 < (G * i,(j + 1)) `2 by A2, A3, A4, Th5;
then ( (G * i,j) `2 <= p `2 & p `2 <= (G * i,(j + 1)) `2 ) by A5, TOPREAL1:10;
then p in { |[r,s]| where r, s is Real : ( (G * i,j) `2 <= s & s <= (G * i,(j + 1)) `2 ) } by A6;
hence x in h_strip G,j by A1, A3, A4, A7, Th6; :: thesis: verum