let i, j be Element of NAT ; 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); ( 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
and
A6:
j < width G
; 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 set ; TARSKI:def 3 ( 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))
; x in v_strip G,i
then reconsider p = x as Point of (TOP-REAL 2) ;
A10:
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
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, Th3
.=
(G * (i + 1),(j + 1)) `1
by A2, A7, A8, A11, A12, Th3
;
now per cases
( i = 0 or i > 0 )
by NAT_1:3;
suppose A14:
i = 0
;
x in v_strip G,ithen
p `1 <= (G * 1,j) `1
by A9, A13, TOPREAL1:9;
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, Th11;
verum end; suppose
i > 0
;
x in v_strip G,ithen A15:
0 + 1
<= i
by NAT_1:13;
A16:
(G * (i + 1),j) `1 <= p `1
by A9, A13, TOPREAL1:9;
A17:
p `1 <= (G * (i + 1),j) `1
by A9, A13, TOPREAL1:9;
then A18:
p `1 = (G * (i + 1),j) `1
by A16, XXREAL_0:1;
i < i + 1
by XREAL_1:31;
then
(G * i,j) `1 < p `1
by A3, A5, A6, A12, A15, A18, Th4;
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, Th9;
verum end;
hence
x in v_strip G,i
; verum