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 & j <= width G ) and
A4: ( 1 <= i & 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 A5: 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) ;
A6: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A7: i < len G by A4, NAT_1:13;
i < i + 1 by XREAL_1:31;
then (G * i,j) `1 < (G * (i + 1),j) `1 by A2, A3, A4, Th4;
then ( (G * i,j) `1 <= p `1 & p `1 <= (G * (i + 1),j) `1 ) by A5, TOPREAL1:9;
then p in { |[r,s]| where r, s is Real : ( (G * i,j) `1 <= r & r <= (G * (i + 1),j) `1 ) } by A6;
hence x in v_strip G,i by A1, A3, A4, A7, Th9; :: thesis: verum