let i, j be Element of NAT ; :: thesis: for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G holds
LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= v_strip G,i
let G be Matrix of (TOP-REAL 2); :: thesis: ( not G is empty-yielding & G is X_equal-in-line & G is X_increasing-in-column & i < len G & 1 <= j & j < width G implies LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= v_strip G,i )
assume that
A1: not G is empty-yielding and
A2: G is X_equal-in-line and
A3: G is X_increasing-in-column and
A4: i < len G and
A5: ( 1 <= j & j < width G ) ; :: thesis: LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= v_strip G,i
A6: ( 1 <= j + 1 & j + 1 <= width G ) by A5, NAT_1:13;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) or x in v_strip G,i )
assume A7: x in LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) ; :: 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: ( 1 <= i + 1 & i + 1 <= len G ) by A4, NAT_1:11, NAT_1:13;
then A10: (G * (i + 1),j) `1 = (G * (i + 1),1) `1 by A2, A5, Th3
.= (G * (i + 1),(j + 1)) `1 by A2, A6, A9, Th3 ;

now

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

suppose A11: i = 0 ; :: thesis: x in v_strip G,i

then p `1 <= (G * 1,j) `1 by A7, A10, TOPREAL1:9;
then p in { |[r,s]| where r, s is Real : r <= (G * 1,j) `1 } by A8;
hence x in v_strip G,i by A1, A2, A5, A11, Th11; :: thesis: verum

end;

suppose i > 0 ; :: thesis: x in v_strip G,i

then A12: 0 + 1 <= i by NAT_1:13;
A13: ( (G * (i + 1),j) `1 <= p `1 & p `1 <= (G * (i + 1),j) `1 ) by A7, A10, TOPREAL1:9;
then A14: p `1 = (G * (i + 1),j) `1 by XXREAL_0:1;
i < i + 1 by XREAL_1:31;
then (G * i,j) `1 < p `1 by A3, A5, A9, A12, A14, Th4;
then p in { |[r,s]| where r, s is Real : ( (G * i,j) `1 <= r & r <= (G * (i + 1),j) `1 ) } by A8, A13;
hence x in v_strip G,i by A2, A4, A5, A12, Th9; :: thesis: verum

end;

end;

end;

hence x in v_strip G,i ; :: thesis: verum