let C be Simple_closed_curve; :: thesis:
let p be Point of (TOP-REAL 2); :: thesis:
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:
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:
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;

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 A1, A7, A8, A10, A14, Th10, Th12, XXREAL_0:2; :: thesis:
cell ((Gauge (C,n)),I,J) c= Ball (P,r) by A2, A4, A5, A9, A7, A6, A8, 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 A3, A9, A7, A6, A8, A20, A17, A19, A18, A12, A22, JORDAN9:17; :: thesis:

end;

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

then A24: p `1 <= ((Gauge (C,n)) * (((I -' 1) + 1),J)) `1 by A9, XREAL_1:235;
A25: (I -' 1) + 1 <= len (Gauge (C,n)) by A9, A11, XREAL_1:235;
A26: 1 <= J by A1, Th12;
A27: 1 <= I -' 1 by A1, Th10, NAT_D:49;
then I -' 1 < I by NAT_D:51;
then A28: p `1 > ((Gauge (C,n)) * ((I -' 1),J)) `1 by A11, A15, A23, A27, A26, GOBOARD5:3;
take I -' 1 ; :: thesis:
take J ; :: thesis:
A29: J + 1 <= width (Gauge (C,n)) by A1, Th12;
A30: 1 <= I -' 1 by A1, Th10, NAT_D:49;
then A31: I -' 1 < I by NAT_D:51;
len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def 1;
then A32: J <= len (Gauge (C,n)) by A8, A14, 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 A6, A32, JORDAN8:11;
then p `1 <= W-bound (BDD C) by A1, A23, Th6;
then A33: p `1 < W-bound (BDD C) by A1, Th22, XXREAL_0:1;
BDD C is bounded by JORDAN2C:106;
hence contradiction by A1, A33, Th5; :: thesis:

end;

hence ( 1 < I -' 1 & I -' 1 < len (Gauge (C,n)) & 1 < J & J < width (Gauge (C,n)) ) by A1, A14, A11, A30, A29, A31, Th12, XXREAL_0:1, XXREAL_0:2; :: thesis:
A34: (I -' 1) + 1 <= len (Gauge (C,n)) by A9, A11, XREAL_1:235;
A35: J + 1 <= width (Gauge (C,n)) by A1, Th12;
A36: p `1 <= ((Gauge (C,n)) * (((I -' 1) + 1),J)) `1 by A9, A23, XREAL_1:235;
A37: 1 <= J by A1, Th12;
A38: (I -' 1) + 1 = I by A9, XREAL_1:235;
then A39: ((Gauge (C,n)) * ((I -' 1),J)) `2 = ((Gauge (C,n)) * (I,J)) `2 by A11, A30, A37, A29, JORDAN9:16;
A40: ((Gauge (C,n)) * ((I -' 1),(J + 1))) `2 = ((Gauge (C,n)) * (I,(J + 1))) `2 by A11, A38, A30, A37, A29, JORDAN9:16;
p `1 > ((Gauge (C,n)) * ((I -' 1),J)) `1 by A11, A15, A23, A30, A37, A31, GOBOARD5:3;
then p in cell ((Gauge (C,n)),(I -' 1),J) by A19, A13, A30, A34, A37, A29, A36, A39, A40, JORDAN9:17;
then cell ((Gauge (C,n)),(I -' 1),J) c= Ball (P,r) by A2, A4, A5, A27, A25, A26, A35, 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 A3, A19, A13, A39, A40, A27, A25, A26, A35, A24, A28, JORDAN9:17; :: thesis:

end;