let i, j be Nat; :: thesis: for G being Matrix of (TOP-REAL 2) st 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: ( 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: 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 and
A6: j < width G ; :: thesis: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= v_strip (G,i)
A7: 1 <= j + 1 by A5, NAT_1:13;
A8: j + 1 <= width G by A6, NAT_1:13;
let x be object ; :: 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 A9: 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) ;
A10: p = |[(p `1),(p `2)]| by EUCLID:53;
A11: 1 <= i + 1 by NAT_1:11;
A12: i + 1 <= len G by A4, NAT_1:13;
then A13: (G * ((i + 1),j)) `1 = (G * ((i + 1),1)) `1 by A2, A5, A6, A11, Th2
.= (G * ((i + 1),(j + 1))) `1 by A2, A7, A8, A11, A12, Th2 ;

now :: thesis: x in v_strip (G,i)

per cases ( i = 0 or i > 0 ) ;

suppose A14: i = 0 ; :: thesis: x in v_strip (G,i)

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

end;

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

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

end;

end;

end;

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