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