let C be Simple_closed_curve; :: thesis:
let p be Point of (TOP-REAL 2); :: thesis:
assume A1: p in BDD C ; :: thesis:
reconsider P = p as Point of (Euclid 2) by Lm3;
consider r being Real such that
A2: ( r > 0 & Ball P,r c= BDD C ) by A1, Th29;
set l = r / 4;
r / 4 > 0 by A2, XREAL_1:141;
then consider n being Element of NAT such that
1 < n and
A3: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4 and
A4: dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4 by GOBRD14:21;
take n ; :: thesis:
set G = Gauge C,n;
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);
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)/];
A5: ( 1 < [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] & [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] + 1 <= len (Gauge C,n) ) by A1, Th22, Th23;
A6: ( 1 < [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] & [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] + 1 <= width (Gauge C,n) ) by A1, Th24;
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 A5, INT_1:16;
A7: (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1)) > p `2 by Th28;
A8: ( 1 <= I + 1 & 1 <= J + 1 ) by NAT_1:11;
A9: ( I < I + 1 & J < J + 1 ) by XREAL_1:31;
then A10: ( I <= len (Gauge C,n) & J <= width (Gauge C,n) ) by A5, A6, XXREAL_0:2;
then [I,J] in Indices (Gauge C,n) by A5, A6, MATRIX_1:37;
then (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)) & ((Gauge C,n) * I,J) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) ) by EUCLID:56;
then A11: ( ((Gauge C,n) * I,J) `1 <= p `1 & ((Gauge C,n) * I,J) `2 <= p `2 ) by Th25, Th27;
[(I + 1),J] in Indices (Gauge C,n) by A1, Th23, A6, A8, A10, MATRIX_1:37;
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:56;
then A12: p `1 < ((Gauge C,n) * (I + 1),J) `1 by Th26;
[I,(J + 1)] in Indices (Gauge C,n) by A5, A1, Th24, A8, A10, MATRIX_1:37;
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 A13: ((Gauge C,n) * I,(J + 1)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1)) by EUCLID:56;
then A14: p `2 < ((Gauge C,n) * I,(J + 1)) `2 by Th28;
A15: p in cell (Gauge C,n),I,J by A5, A6, A7, A11, A12, A13, JORDAN9:19;
reconsider GIJ = (Gauge C,n) * I,J as Point of (Euclid 2) by Lm3;
GIJ in cell (Gauge C,n),I,J by A5, A6, JORDAN9:22;
then A16: dist ((Gauge C,n) * I,J),p <= 2 * (r / 4) by A3, A4, A5, A6, A15, Th30;
A17: 2 * (r / 4) < r by A2, Lm4;
then dist ((Gauge C,n) * I,J),p < r by A16, XXREAL_0:2;
then dist GIJ,P < r by TOPREAL6:def 1;
then A18: GIJ in Ball P,r by METRIC_1:12;
reconsider GIJ = (Gauge C,n) * (I + 1),J as Point of (Euclid 2) by Lm3;
GIJ in cell (Gauge C,n),I,J by A5, A6, JORDAN9:22;
then dist ((Gauge C,n) * (I + 1),J),p <= 2 * (r / 4) by A3, A4, A5, A6, A15, Th30;
then dist ((Gauge C,n) * (I + 1),J),p < r by A17, XXREAL_0:2;
then dist GIJ,P < r by TOPREAL6:def 1;
then A19: GIJ in Ball P,r by METRIC_1:12;
reconsider GIJ = (Gauge C,n) * (I + 1),(J + 1) as Point of (Euclid 2) by Lm5;
GIJ in cell (Gauge C,n),I,J by A5, A6, JORDAN9:22;
then dist ((Gauge C,n) * (I + 1),(J + 1)),p <= 2 * (r / 4) by A3, A4, A5, A6, A15, Th30;
then dist ((Gauge C,n) * (I + 1),(J + 1)),p < r by A17, XXREAL_0:2;
then A20: dist GIJ,P < r by TOPREAL6:def 1;
reconsider GIJ = (Gauge C,n) * I,(J + 1) as Point of (Euclid 2) by Lm5;
GIJ in cell (Gauge C,n),I,J by A5, A6, JORDAN9:22;
then dist ((Gauge C,n) * I,(J + 1)),p <= 2 * (r / 4) by A3, A4, A5, A6, A15, Th30;
then dist ((Gauge C,n) * I,(J + 1)),p < r by A17, XXREAL_0:2;
then dist GIJ,P < r by TOPREAL6:def 1;
then A21: ( (Gauge C,n) * I,(J + 1) in Ball P,r & (Gauge C,n) * (I + 1),(J + 1) in Ball P,r ) by A20, METRIC_1:12;

per cases ;

suppose A22: p `1 <> ((Gauge C,n) * I,J) `1 ; :: thesis:

take I ; :: thesis:
take J ; :: thesis:
thus ( 1 < I & I < len (Gauge C,n) & 1 < J & J < width (Gauge C,n) ) by A5, A6, A9, XXREAL_0:2; :: thesis:
cell (Gauge C,n),I,J c= Ball P,r by A2, A3, A4, A5, A6, A15, A18, A19, A21, Lm6;
hence ( 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 ) by A2, A5, A6, A7, A11, A12, A13, A22, JORDAN9:19, XBOOLE_1:1; :: thesis:

end;

suppose A23: p `1 = ((Gauge C,n) * I,J) `1 ; :: thesis:

set q = (Gauge C,n) * (I -' 1),J;
reconsider GIJ = (Gauge C,n) * (I -' 1),J as Point of (Euclid 2) by Lm3;
A24: (I -' 1) + 1 = I by A5, XREAL_1:237;
A25: ( 1 <= I -' 1 & (I -' 1) + 1 <= len (Gauge C,n) & 1 <= J & J + 1 <= width (Gauge C,n) ) by A1, A5, A10, Th24, NAT_D:49, XREAL_1:237;
then A26: GIJ in cell (Gauge C,n),(I -' 1),J by JORDAN9:22;
A27: I -' 1 < I by A25, NAT_D:51;
then A28: ( p `1 <= ((Gauge C,n) * ((I -' 1) + 1),J) `1 & p `1 > ((Gauge C,n) * (I -' 1),J) `1 ) by A5, A10, A23, A25, GOBOARD5:4, XREAL_1:237;
A29: ((Gauge C,n) * (I -' 1),J) `2 = ((Gauge C,n) * I,J) `2 by A24, A25, JORDAN9:18;
A30: ((Gauge C,n) * (I -' 1),(J + 1)) `2 = ((Gauge C,n) * I,(J + 1)) `2 by A24, A25, JORDAN9:18;
then A31: p in cell (Gauge C,n),(I -' 1),J by A11, A14, A25, A28, A29, JORDAN9:19;
then dist p,((Gauge C,n) * (I -' 1),J) < 2 * (r / 4) by A3, A4, A25, A26, Th30;
then dist ((Gauge C,n) * (I -' 1),J),p < r by A17, XXREAL_0:2;
then dist GIJ,P < r by TOPREAL6:def 1;
then A32: GIJ in Ball P,r by METRIC_1:12;
take I -' 1 ; :: thesis:
take J ; :: thesis:
len (Gauge C,n) = width (Gauge C,n) by JORDAN8:def 1;
then A33: ( 1 <= J & J <= len (Gauge C,n) ) by A6, A9, XXREAL_0:2;
I -' 1 <> 1

proof

assume I -' 1 = 1 ; :: thesis:
then 1 = I - 1 by NAT_D:39;
then ((Gauge C,n) * I,J) `1 = W-bound C by A33, JORDAN8:14;
then A34: p `1 <= W-bound (BDD C) by A1, A23, Th18;
p `1 <> W-bound (BDD C) by A1, Th34;
then A35: p `1 < W-bound (BDD C) by A34, XXREAL_0:1;
BDD C is Bounded by JORDAN2C:114;
hence contradiction by A1, A35, Th6; :: thesis:

end;

hence ( 1 < I -' 1 & I -' 1 < len (Gauge C,n) & 1 < J & J < width (Gauge C,n) ) by A1, A9, A10, A25, A27, Th24, XXREAL_0:1, XXREAL_0:2; :: thesis:
set q = (Gauge C,n) * (I -' 1),(J + 1);
reconsider GIJ = (Gauge C,n) * (I -' 1),(J + 1) as Point of (Euclid 2) by Lm3;
A36: ( 1 <= I -' 1 & (I -' 1) + 1 <= len (Gauge C,n) & 1 <= J & J + 1 <= width (Gauge C,n) ) by A1, A5, A10, Th24, NAT_D:49, XREAL_1:237;
then A37: GIJ in cell (Gauge C,n),(I -' 1),J by JORDAN9:22;
I -' 1 < I by A36, NAT_D:51;
then A38: ( p `1 <= ((Gauge C,n) * ((I -' 1) + 1),J) `1 & p `1 > ((Gauge C,n) * (I -' 1),J) `1 ) by A5, A10, A23, A36, GOBOARD5:4, XREAL_1:237;
then p in cell (Gauge C,n),(I -' 1),J by A11, A14, A29, A30, A36, JORDAN9:19;
then dist ((Gauge C,n) * (I -' 1),(J + 1)),p < 2 * (r / 4) by A3, A4, A36, A37, Th30;
then dist ((Gauge C,n) * (I -' 1),(J + 1)),p < r by A17, XXREAL_0:2;
then dist GIJ,P < r by TOPREAL6:def 1;
then ( (Gauge C,n) * ((I -' 1) + 1),J in Ball P,r & (Gauge C,n) * (I -' 1),(J + 1) in Ball P,r & (Gauge C,n) * ((I -' 1) + 1),(J + 1) in Ball P,r ) by A5, A18, A21, METRIC_1:12, XREAL_1:237;
then cell (Gauge C,n),(I -' 1),J c= Ball P,r by A2, A3, A4, A31, A32, A36, Lm6;
hence ( p `1 <> ((Gauge C,n) * (I -' 1),J) `1 & p in cell (Gauge C,n),(I -' 1),J & cell (Gauge C,n),(I -' 1),J c= BDD C ) by A2, A11, A14, A29, A30, A36, A38, JORDAN9:19, XBOOLE_1:1; :: thesis:

end;