let C be Simple_closed_curve; :: thesis: for p being Point of (TOP-REAL 2) st p in BDD C holds
ex n, i, j being Nat st
( 1 < i & i < len (Gauge (C,n)) & 1 < j & j < width (Gauge (C,n)) & p `1 <> ((Gauge (C,n)) * (i,j)) `1 & p in cell ((Gauge (C,n)),i,j) & cell ((Gauge (C,n)),i,j) c= BDD C )
let p be Point of (TOP-REAL 2); :: thesis: ( p in BDD C implies ex n, i, j being Nat st
( 1 < i & i < len (Gauge (C,n)) & 1 < j & j < width (Gauge (C,n)) & p `1 <> ((Gauge (C,n)) * (i,j)) `1 & p in cell ((Gauge (C,n)),i,j) & cell ((Gauge (C,n)),i,j) c= BDD C ) )
reconsider P = p as Point of (Euclid 2) by Lm3;
set W = W-bound C;
set E = E-bound C;
set S = S-bound C;
set N = N-bound C;
set EW = (E-bound C) - (W-bound C);
set NS = (N-bound C) - (S-bound C);
assume A1: p in BDD C ; :: thesis: ex n, i, j being Nat st
( 1 < i & i < len (Gauge (C,n)) & 1 < j & j < width (Gauge (C,n)) & p `1 <> ((Gauge (C,n)) * (i,j)) `1 & p in cell ((Gauge (C,n)),i,j) & cell ((Gauge (C,n)),i,j) c= BDD C )
then consider r being Real such that
A2: r > 0 and
A3: Ball (P,r) c= BDD C by Th17;
set l = r / 4;
r / 4 > 0 by A2, XREAL_1:139;
then consider n being Nat such that
1 < n and
A4: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 and
A5: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 by GOBRD14:11;
set I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/];
set J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/];
A6: 1 < [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] by A1, Th12;
set G = Gauge (C,n);
A7: [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] + 1 <= len (Gauge (C,n)) by A1, Th11;
A8: [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] + 1 <= width (Gauge (C,n)) by A1, Th12;
take n ; :: thesis: ex i, j being Nat st
( 1 < i & i < len (Gauge (C,n)) & 1 < j & j < width (Gauge (C,n)) & p `1 <> ((Gauge (C,n)) * (i,j)) `1 & p in cell ((Gauge (C,n)),i,j) & cell ((Gauge (C,n)),i,j) c= BDD C )
A9: 1 < [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] by A1, Th10;
then reconsider I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/], J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] as Element of NAT by A6, INT_1:3;
A10: I < I + 1 by XREAL_1:29;
then A11: I <= len (Gauge (C,n)) by A7, XXREAL_0:2;
1 <= J + 1 by NAT_1:11;
then [I,(J + 1)] in Indices (Gauge (C,n)) by A9, A8, A11, MATRIX_0:30;
then (Gauge (C,n)) * (I,(J + 1)) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((J + 1) - 2)))]| by JORDAN8:def 1;
then A12: ((Gauge (C,n)) * (I,(J + 1))) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1)) by EUCLID:52;
then A13: p `2 < ((Gauge (C,n)) * (I,(J + 1))) `2 by Th16;
A14: J < J + 1 by XREAL_1:29;
then A15: J <= width (Gauge (C,n)) by A8, XXREAL_0:2;
then [I,J] in Indices (Gauge (C,n)) by A9, A6, A11, MATRIX_0:30;
then A16: (Gauge (C,n)) * (I,J) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)))]| by JORDAN8:def 1;
then ((Gauge (C,n)) * (I,J)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) by EUCLID:52;
then A17: ((Gauge (C,n)) * (I,J)) `1 <= p `1 by Th13;
1 <= I + 1 by NAT_1:11;
then [(I + 1),J] in Indices (Gauge (C,n)) by A7, A6, A15, MATRIX_0:30;
then (Gauge (C,n)) * ((I + 1),J) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((I + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)))]| by JORDAN8:def 1;
then ((Gauge (C,n)) * ((I + 1),J)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1)) by EUCLID:52;
then A18: p `1 < ((Gauge (C,n)) * ((I + 1),J)) `1 by Th14;
((Gauge (C,n)) * (I,J)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) by A16, EUCLID:52;
then A19: ((Gauge (C,n)) * (I,J)) `2 <= p `2 by Th15;
A20: (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1)) > p `2 by Th16;
then A21: p in cell ((Gauge (C,n)),I,J) by A9, A7, A6, A8, A17, A19, A18, A12, JORDAN9:17;