let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for i, n being Nat st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,0) misses C
let i, n be Nat; :: thesis: ( i <= len (Gauge (C,n)) implies cell ((Gauge (C,n)),i,0) misses C )
set G = Gauge (C,n);
assume A1: i <= len (Gauge (C,n)) ; :: thesis: cell ((Gauge (C,n)),i,0) misses C
A2: len (Gauge (C,n)) = width (Gauge (C,n)) by Def1;
assume (cell ((Gauge (C,n)),i,0)) /\ C <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A3: p in (cell ((Gauge (C,n)),i,0)) /\ C by SUBSET_1:4;
A4: p in cell ((Gauge (C,n)),i,0) by A3, XBOOLE_0:def 4;
A5: p in C by A3, XBOOLE_0:def 4;
4 <= len (Gauge (C,n)) by Th10;
then A6: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
set NS = ((N-bound C) - (S-bound C)) / (2 |^ n);
[1,1] in Indices (Gauge (C,n)) by A2, A6, MATRIX_0:30;
then (Gauge (C,n)) * (1,1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]| by Def1;
then A7: ((Gauge (C,n)) * (1,1)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (- 1)) by EUCLID:52;
A8: 2 |^ n > 0 by NEWTON:83;
N-bound C > S-bound C by Th9;
then (N-bound C) - (S-bound C) > 0 by XREAL_1:50;
then ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A8, XREAL_1:139;
then (((N-bound C) - (S-bound C)) / (2 |^ n)) * (- 1) < 0 * (- 1) by XREAL_1:69;
then A9: ((Gauge (C,n)) * (1,1)) `2 < (S-bound C) + 0 by A7, XREAL_1:6;
A10: ( i = 0 or i >= 1 + 0 ) by NAT_1:9;

per cases ( i = 0 or i = len (Gauge (C,n)) or ( 1 <= i & i < len (Gauge (C,n)) ) ) by A1, A10, XXREAL_0:1;

suppose i = 0 ; :: thesis: contradiction

then cell ((Gauge (C,n)),i,0) = { |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & s <= ((Gauge (C,n)) * (1,1)) `2 ) } by GOBRD11:24;
then consider r, s being Real such that
A11: p = |[r,s]| and
r <= ((Gauge (C,n)) * (1,1)) `1 and
A12: s <= ((Gauge (C,n)) * (1,1)) `2 by A4;
p `2 = s by A11, EUCLID:52;
then S-bound C > p `2 by A9, A12, XXREAL_0:2;
hence contradiction by A5, PSCOMP_1:24; :: thesis: verum

end;

suppose i = len (Gauge (C,n)) ; :: thesis: contradiction

then cell ((Gauge (C,n)),i,0) = { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r & s <= ((Gauge (C,n)) * (1,1)) `2 ) } by GOBRD11:27;
then consider r, s being Real such that
A13: p = |[r,s]| and
((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r and
A14: s <= ((Gauge (C,n)) * (1,1)) `2 by A4;
p `2 = s by A13, EUCLID:52;
then S-bound C > p `2 by A9, A14, XXREAL_0:2;
hence contradiction by A5, PSCOMP_1:24; :: thesis: verum

end;

suppose ( 1 <= i & i < len (Gauge (C,n)) ) ; :: thesis: contradiction

then cell ((Gauge (C,n)),i,0) = { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i + 1),1)) `1 & s <= ((Gauge (C,n)) * (1,1)) `2 ) } by GOBRD11:30;
then consider r, s being Real such that
A15: p = |[r,s]| and
((Gauge (C,n)) * (i,1)) `1 <= r and
r <= ((Gauge (C,n)) * ((i + 1),1)) `1 and
A16: s <= ((Gauge (C,n)) * (1,1)) `2 by A4;
p `2 = s by A15, EUCLID:52;
then S-bound C > p `2 by A9, A16, XXREAL_0:2;
hence contradiction by A5, PSCOMP_1:24; :: thesis: verum

end;

end;