let i, j be Nat; for G being Matrix of (TOP-REAL 2) st G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G holds
LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i)
let G be Matrix of (TOP-REAL 2); ( G is V3() & G is X_equal-in-line & G is X_increasing-in-column & 1 <= i & i <= len G & 1 <= j & j < width G implies LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i) )
assume that
A1:
G is V3()
and
A2:
G is X_equal-in-line
and
A3:
G is X_increasing-in-column
and
A4:
1 <= i
and
A5:
i <= len G
and
A6:
1 <= j
and
A7:
j < width G
; LSeg ((G * (i,j)),(G * (i,(j + 1)))) c= v_strip (G,i)
A8:
1 <= j + 1
by A6, NAT_1:13;
A9:
j + 1 <= width G
by A7, NAT_1:13;
let x be object ; TARSKI:def 3 ( not x in LSeg ((G * (i,j)),(G * (i,(j + 1)))) or x in v_strip (G,i) )
assume A10:
x in LSeg ((G * (i,j)),(G * (i,(j + 1))))
; x in v_strip (G,i)
then reconsider p = x as Point of (TOP-REAL 2) ;
A11:
p = |[(p `1),(p `2)]|
by EUCLID:53;
A12: (G * (i,j)) `1 =
(G * (i,1)) `1
by A2, A4, A5, A6, A7, Th2
.=
(G * (i,(j + 1))) `1
by A2, A4, A5, A8, A9, Th2
;
now x in v_strip (G,i)per cases
( i = len G or i < len G )
by A5, XXREAL_0:1;
suppose A13:
i = len G
;
x in v_strip (G,i)then
(G * ((len G),j)) `1 <= p `1
by A10, A12, TOPREAL1:3;
then
p in { |[r,s]| where r, s is Real : (G * ((len G),j)) `1 <= r }
by A11;
hence
x in v_strip (
G,
i)
by A1, A2, A6, A7, A13, Th9;
verum end; suppose A14:
i < len G
;
x in v_strip (G,i)then A15:
i + 1
<= len G
by NAT_1:13;
A16:
(G * (i,j)) `1 <= p `1
by A10, A12, TOPREAL1:3;
p `1 <= (G * (i,j)) `1
by A10, A12, TOPREAL1:3;
then A17:
p `1 = (G * (i,j)) `1
by A16, XXREAL_0:1;
i < i + 1
by XREAL_1:29;
then
p `1 < (G * ((i + 1),j)) `1
by A3, A4, A6, A7, A15, A17, Th3;
then
p in { |[r,s]| where r, s is Real : ( (G * (i,j)) `1 <= r & r <= (G * ((i + 1),j)) `1 ) }
by A11, A16;
hence
x in v_strip (
G,
i)
by A2, A4, A6, A7, A14, Th8;
verum end; end; end;
hence
x in v_strip (G,i)
; verum