let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for j, n being Nat st j <= len (Gauge C,n) holds
cell (Gauge C,n),0 ,j misses C
let j, n be Nat; :: thesis: ( j <= len (Gauge C,n) implies cell (Gauge C,n),0 ,j misses C )
set G = Gauge C,n;
A1: j in NAT by ORDINAL1:def 13;
assume A2: j <= len (Gauge C,n) ; :: thesis: cell (Gauge C,n),0 ,j misses C
A3: ( len (Gauge C,n) = (2 |^ n) + (1 + 2) & len (Gauge C,n) = width (Gauge C,n) ) by Def1;
assume (cell (Gauge C,n),0 ,j) /\ C <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider p being Point of (TOP-REAL 2) such that
A4: p in (cell (Gauge C,n),0 ,j) /\ C by SUBSET_1:10;
A5: ( p in cell (Gauge C,n),0 ,j & p in C ) by A4, XBOOLE_0:def 4;
4 <= len (Gauge C,n) by Th13;
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 EW = ((E-bound C) - (W-bound C)) / (2 |^ n);
[1,1] in Indices (Gauge C,n) by A3, A6, MATRIX_1:37;
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) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (- 1)) by EUCLID:56;
A8: 2 |^ n > 0 by NEWTON:102;
E-bound C > W-bound C by Th11;
then (E-bound C) - (W-bound C) > 0 by XREAL_1:52;
then ((E-bound C) - (W-bound C)) / (2 |^ n) > 0 by A8, XREAL_1:141;
then (((E-bound C) - (W-bound C)) / (2 |^ n)) * (- 1) < 0 * (- 1) by XREAL_1:71;
then A9: ((Gauge C,n) * 1,1) `1 < (W-bound C) + 0 by A7, XREAL_1:8;
( j = 0 or j > 0 ) by NAT_1:3;
then A10: ( j = 0 or j >= 1 + 0 ) by NAT_1:9;

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

suppose j = 0 ; :: thesis: contradiction

then cell (Gauge C,n),0 ,j = { |[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
A12: ( r <= ((Gauge C,n) * 1,1) `1 & s <= ((Gauge C,n) * 1,1) `2 ) by A5;
p `1 = r by A11, EUCLID:56;
then ( W-bound C > p `1 & p `1 >= W-bound C ) by A5, A9, A12, PSCOMP_1:71, XXREAL_0:2;
hence contradiction ; :: thesis: verum

end;

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

then cell (Gauge C,n),0 ,j = { |[r,s]| where r, s is Real : ( r <= ((Gauge C,n) * 1,1) `1 & ((Gauge C,n) * 1,(width (Gauge C,n))) `2 <= s ) } by A3, GOBRD11:25;
then consider r, s being Real such that
A13: p = |[r,s]| and
A14: ( r <= ((Gauge C,n) * 1,1) `1 & ((Gauge C,n) * 1,(width (Gauge C,n))) `2 <= s ) by A5;
p `1 = r by A13, EUCLID:56;
then ( W-bound C > p `1 & p `1 >= W-bound C ) by A5, A9, A14, PSCOMP_1:71, XXREAL_0:2;
hence contradiction ; :: thesis: verum

end;

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

then cell (Gauge C,n),0 ,j = { |[r,s]| where r, s is Real : ( r <= ((Gauge C,n) * 1,1) `1 & ((Gauge C,n) * 1,j) `2 <= s & s <= ((Gauge C,n) * 1,(j + 1)) `2 ) } by A1, A3, GOBRD11:26;
then consider r, s being Real such that
A15: p = |[r,s]| and
A16: ( r <= ((Gauge C,n) * 1,1) `1 & ((Gauge C,n) * 1,j) `2 <= s & s <= ((Gauge C,n) * 1,(j + 1)) `2 ) by A5;
p `1 = r by A15, EUCLID:56;
then ( W-bound C > p `1 & p `1 >= W-bound C ) by A5, A9, A16, PSCOMP_1:71, XXREAL_0:2;
hence contradiction ; :: thesis: verum

end;

end;