let j, i be Element of NAT ; for G being Matrix of (TOP-REAL 2) st not G is empty-yielding & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G holds
LSeg (G * i,j),(G * (i + 1),j) c= h_strip G,j
let G be Matrix of (TOP-REAL 2); ( not G is empty-yielding & G is Y_equal-in-column & G is Y_increasing-in-line & 1 <= j & j <= width G & 1 <= i & i < len G implies LSeg (G * i,j),(G * (i + 1),j) c= h_strip G,j )
assume that
A1:
not G is empty-yielding
and
A2:
G is Y_equal-in-column
and
A3:
G is Y_increasing-in-line
and
A4:
1 <= j
and
A5:
j <= width G
and
A6:
1 <= i
and
A7:
i < len G
; LSeg (G * i,j),(G * (i + 1),j) c= h_strip G,j
A8:
1 <= i + 1
by A6, NAT_1:13;
A9:
i + 1 <= len G
by A7, NAT_1:13;
let x be set ; TARSKI:def 3 ( not x in LSeg (G * i,j),(G * (i + 1),j) or x in h_strip G,j )
assume A10:
x in LSeg (G * i,j),(G * (i + 1),j)
; x in h_strip G,j
then reconsider p = x as Point of (TOP-REAL 2) ;
A11:
p = |[(p `1 ),(p `2 )]|
by EUCLID:57;
A12: (G * i,j) `2 =
(G * 1,j) `2
by A2, A4, A5, A6, A7, Th2
.=
(G * (i + 1),j) `2
by A2, A4, A5, A8, A9, Th2
;
now per cases
( j = width G or j < width G )
by A5, XXREAL_0:1;
suppose A13:
j = width G
;
x in h_strip G,jthen
(G * i,(width G)) `2 <= p `2
by A10, A12, TOPREAL1:10;
then
p in { |[r,s]| where r, s is Real : (G * i,(width G)) `2 <= s }
by A11;
hence
x in h_strip G,
j
by A1, A2, A6, A7, A13, Th7;
verum end; suppose A14:
j < width G
;
x in h_strip G,jthen A15:
j + 1
<= width G
by NAT_1:13;
A16:
(G * i,j) `2 <= p `2
by A10, A12, TOPREAL1:10;
p `2 <= (G * i,j) `2
by A10, A12, TOPREAL1:10;
then A17:
p `2 = (G * i,j) `2
by A16, XXREAL_0:1;
j < j + 1
by XREAL_1:31;
then
p `2 < (G * i,(j + 1)) `2
by A3, A4, A6, A7, A15, A17, Th5;
then
p in { |[r,s]| where r, s is Real : ( (G * i,j) `2 <= s & s <= (G * i,(j + 1)) `2 ) }
by A11, A16;
hence
x in h_strip G,
j
by A2, A4, A6, A7, A14, Th6;
verum end;
hence
x in h_strip G,j
; verum