:: JORDAN1C semantic presentation

begin


Lm1: now__::_thesis:_for_r_being_real_number_
for_j_being_Element_of_NAT_holds_[\(r_+_j)/]_-_j_=_[\r/]
let r be real number ; ::_thesis: for j being Element of NAT holds [\(r + j)/] - j = [\r/]
let j be Element of NAT ; ::_thesis: [\(r + j)/] - j = [\r/]
thus [\(r + j)/] - j = ([\r/] + j) - j by INT_1:28
.= [\r/] ; ::_thesis: verum
end;

Lm2:  for a, b, c being real number st a <> 0 & b <> 0 holds
(a / b) * ((c / a) * b) = c
proof
let a, b, c be real number ; ::_thesis: ( a <> 0 & b <> 0 implies (a / b) * ((c / a) * b) = c )
assume that
A1: a <> 0 and
A2: b <> 0 ; ::_thesis: (a / b) * ((c / a) * b) = c
(a / b) * ((c / a) * b) = ((a / b) * b) * (c / a)
.= a * (c / a) by A2, XCMPLX_1:87
.= c by A1, XCMPLX_1:87 ;
hence  (a / b) * ((c / a) * b) = c ; ::_thesis: verum
end;

Lm3:  for p being Point of (TOP-REAL 2) holds p is Point of (Euclid 2)
proof
let p be Point of (TOP-REAL 2); ::_thesis: p is Point of (Euclid 2)
 TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by EUCLID:def_8;
then  TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) by PCOMPS_1:def_5;
hence  p is Point of (Euclid 2) ; ::_thesis: verum
end;

Lm4:  for r being real number st r > 0 holds
2 * (r / 4) < r
proof
let r be real number ; ::_thesis: ( r > 0 implies 2 * (r / 4) < r )
A1: 2 * (r / 4) = r / 2 ;
assume  r > 0 ; ::_thesis: 2 * (r / 4) < r
hence  2 * (r / 4) < r by A1, XREAL_1:216; ::_thesis: verum
end;

theorem Th1: :: JORDAN1C:1
for C being Simple_closed_curve
for i, j, n being Element of NAT st [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) = (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1)
proof
let C be Simple_closed_curve; ::_thesis: for i, j, n being Element of NAT st [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) = (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1)
let i, j, n be Element of NAT ; ::_thesis: ( [i,j] in Indices (Gauge (C,n)) & [(i + 1),j] in Indices (Gauge (C,n)) implies dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) = (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1) )
set G = Gauge (C,n);
assume that
A1: [i,j] in Indices (Gauge (C,n)) and
A2: [(i + 1),j] in Indices (Gauge (C,n)) ; ::_thesis: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) = (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1)
A3: j <= width (Gauge (C,n)) by A1, MATRIX_1:38;
 1 <= j by A1, MATRIX_1:38;
then A4: 1 <= width (Gauge (C,n)) by A3, XXREAL_0:2;
A5: len (Gauge (C,n)) >= 4 by JORDAN8:10;
then  2 <= len (Gauge (C,n)) by XXREAL_0:2;
then A6: [2,1] in Indices (Gauge (C,n)) by A4, MATRIX_1:36;
A7: dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) = ((E-bound C) - (W-bound C)) / (2 |^ n) by A1, A2, GOBRD14:10;
 1 <= len (Gauge (C,n)) by A5, XXREAL_0:2;
then  [1,1] in Indices (Gauge (C,n)) by A4, MATRIX_1:36;
then  dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * ((1 + 1),1))) = dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * ((i + 1),j))) by A6, A7, GOBRD14:10
.= (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1) by A1, A2, GOBRD14:5 ;
hence  dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) = (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1) ; ::_thesis: verum
end;

theorem Th2: :: JORDAN1C:2
for C being Simple_closed_curve
for i, j, n being Element of NAT st [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) = (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2)
proof
let C be Simple_closed_curve; ::_thesis: for i, j, n being Element of NAT st [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) holds
dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) = (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2)
let i, j, n be Element of NAT ; ::_thesis: ( [i,j] in Indices (Gauge (C,n)) & [i,(j + 1)] in Indices (Gauge (C,n)) implies dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) = (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2) )
set G = Gauge (C,n);
assume that
A1: [i,j] in Indices (Gauge (C,n)) and
A2: [i,(j + 1)] in Indices (Gauge (C,n)) ; ::_thesis: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) = (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2)
A3: 1 <= j + 1 by A2, MATRIX_1:38;
 len (Gauge (C,n)) >= 4 by JORDAN8:10;
then A4: 1 <= len (Gauge (C,n)) by XXREAL_0:2;
 (2 |^ n) + 3 >= 3 by NAT_1:11;
then  width (Gauge (C,n)) >= 3 by JORDAN1A:28;
then  2 <= width (Gauge (C,n)) by XXREAL_0:2;
then A5: [1,2] in Indices (Gauge (C,n)) by A4, MATRIX_1:36;
 j + 1 <= width (Gauge (C,n)) by A2, MATRIX_1:38;
then  1 <= width (Gauge (C,n)) by A3, XXREAL_0:2;
then A6: [1,1] in Indices (Gauge (C,n)) by A4, MATRIX_1:36;
 dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) = ((N-bound C) - (S-bound C)) / (2 |^ n) by A1, A2, GOBRD14:9;
then  dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,(1 + 1)))) = dist (((Gauge (C,n)) * (i,j)),((Gauge (C,n)) * (i,(j + 1)))) by A6, A5, GOBRD14:9
.= (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2) by A1, A2, GOBRD14:6 ;
hence  dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) = (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2) ; ::_thesis: verum
end;

 TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #)
by EUCLID:def_8;

then Lm5:  TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #)
by PCOMPS_1:def_5;

Lm6:  for C being Simple_closed_curve
for i, n, j being Element of NAT
for p being Point of (TOP-REAL 2)
for r being real number
for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) & r > 0 & p = q & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 & p in cell ((Gauge (C,n)),i,j) holds
cell ((Gauge (C,n)),i,j) c= Ball (q,r)
proof
let C be Simple_closed_curve; ::_thesis: for i, n, j being Element of NAT
for p being Point of (TOP-REAL 2)
for r being real number
for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) & r > 0 & p = q & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 & p in cell ((Gauge (C,n)),i,j) holds
cell ((Gauge (C,n)),i,j) c= Ball (q,r)
let i, n, j be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2)
for r being real number
for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) & r > 0 & p = q & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 & p in cell ((Gauge (C,n)),i,j) holds
cell ((Gauge (C,n)),i,j) c= Ball (q,r)
let p be Point of (TOP-REAL 2); ::_thesis: for r being real number
for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) & r > 0 & p = q & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 & p in cell ((Gauge (C,n)),i,j) holds
cell ((Gauge (C,n)),i,j) c= Ball (q,r)
let r be real number ; ::_thesis: for q being Point of (Euclid 2) st 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) & r > 0 & p = q & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 & p in cell ((Gauge (C,n)),i,j) holds
cell ((Gauge (C,n)),i,j) c= Ball (q,r)
let q be Point of (Euclid 2); ::_thesis: ( 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) & r > 0 & p = q & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 & p in cell ((Gauge (C,n)),i,j) implies cell ((Gauge (C,n)),i,j) c= Ball (q,r) )
assume that
A1: 1 <= i and
A2: i + 1 <= len (Gauge (C,n)) and
A3: 1 <= j and
A4: j + 1 <= width (Gauge (C,n)) and
A5: r > 0 and
A6: p = q and
A7: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r / 4 and
A8: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r / 4 and
A9: p in cell ((Gauge (C,n)),i,j) ; ::_thesis: cell ((Gauge (C,n)),i,j) c= Ball (q,r)
set G = Gauge (C,n);
set I = i;
set J = j;
set l = r / 4;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in cell ((Gauge (C,n)),i,j) or x in Ball (q,r) )
assume A10: x in cell ((Gauge (C,n)),i,j) ; ::_thesis: x in Ball (q,r)
then reconsider Q = q, X = x as Point of (TOP-REAL 2) by Lm5;
A11: Q `1 <= ((Gauge (C,n)) * ((i + 1),j)) `1 by A1, A2, A3, A4, A6, A9, JORDAN9:17;
A12: ((Gauge (C,n)) * (i,j)) `2 <= Q `2 by A1, A2, A3, A4, A6, A9, JORDAN9:17;
A13: ((Gauge (C,n)) * (i,j)) `1 <= X `1 by A1, A2, A3, A4, A10, JORDAN9:17;
 j < j + 1 by XREAL_1:29;
then A14: j <= width (Gauge (C,n)) by A4, XXREAL_0:2;
 i < i + 1 by XREAL_1:29;
then A15: i <= len (Gauge (C,n)) by A2, XXREAL_0:2;
then A16: [i,j] in Indices (Gauge (C,n)) by A1, A3, A14, MATRIX_1:36;
A17: X `2 <= ((Gauge (C,n)) * (i,(j + 1))) `2 by A1, A2, A3, A4, A10, JORDAN9:17;
A18: ((Gauge (C,n)) * (i,j)) `2 <= X `2 by A1, A2, A3, A4, A10, JORDAN9:17;
A19: Q `2 <= ((Gauge (C,n)) * (i,(j + 1))) `2 by A1, A2, A3, A4, A6, A9, JORDAN9:17;
A20: X `1 <= ((Gauge (C,n)) * ((i + 1),j)) `1 by A1, A2, A3, A4, A10, JORDAN9:17;
 1 <= j + 1 by A3, XREAL_1:29;
then  [i,(j + 1)] in Indices (Gauge (C,n)) by A1, A4, A15, MATRIX_1:36;
then A21: (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2) < r / 4 by A7, A16, Th2;
 1 <= 1 + i by NAT_1:11;
then  [(i + 1),j] in Indices (Gauge (C,n)) by A2, A3, A14, MATRIX_1:36;
then  (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1) < r / 4 by A8, A16, Th1;
then A22: ((((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1)) + ((((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2)) <= (r / 4) + (r / 4) by A21, XREAL_1:7;
 ((Gauge (C,n)) * (i,j)) `1 <= Q `1 by A1, A2, A3, A4, A6, A9, JORDAN9:17;
then  dist (Q,X) <= ((((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1)) + ((((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2)) by A11, A12, A19, A13, A20, A18, A17, TOPREAL6:95;
then A23: dist (p,X) <= (r / 4) + (r / 4) by A6, A22, XXREAL_0:2;
reconsider x9 = x as Point of (Euclid 2) by A10, Lm3;
 2 * (r / 4) < r by A5, Lm4;
then  dist (X,p) < r by A23, XXREAL_0:2;
then  dist (x9,q) < r by A6, TOPREAL6:def_1;
hence  x in Ball (q,r) by METRIC_1:11; ::_thesis: verum
end;

theorem Th3: :: JORDAN1C:3
for S being Subset of (TOP-REAL 2) st S is bounded holds
proj1 .: S is real-bounded
proof
let S be Subset of (TOP-REAL 2); ::_thesis: ( S is bounded implies proj1 .: S is real-bounded )
assume  S is bounded ; ::_thesis: proj1 .: S is real-bounded
then reconsider C = S as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider r being Real, x being Point of (Euclid 2) such that
A1: 0 < r and
A2: C c= Ball (x,r) by METRIC_6:def_3;
reconsider P = Ball (x,r) as Subset of (TOP-REAL 2) by TOPREAL3:8;
reconsider p = x as Point of (TOP-REAL 2) by TOPREAL3:8;
set t = max ((abs ((p `1) - r)),(abs ((p `1) + r)));
now__::_thesis:_(_abs_((p_`1)_-_r)_<=_0_implies_not_abs_((p_`1)_+_r)_<=_0_)
assume that
A3: abs ((p `1) - r) <= 0 and
A4: abs ((p `1) + r) <= 0 ; ::_thesis: contradiction
 abs ((p `1) - r) = 0 by A3, COMPLEX1:46;
then  abs (r - (p `1)) = 0 by UNIFORM1:11;
then A5: r - (p `1) = 0 by ABSVALUE:2;
 abs ((p `1) + r) = 0 by A4, COMPLEX1:46;
hence  contradiction by A1, A5, ABSVALUE:2; ::_thesis: verum
end;
then A6: max ((abs ((p `1) - r)),(abs ((p `1) + r))) > 0 by XXREAL_0:30;
A7: proj1 .: P = ].((p `1) - r),((p `1) + r).[ by TOPREAL6:43;
 for s being real number st s in proj1 .: S holds
abs s < max ((abs ((p `1) - r)),(abs ((p `1) + r)))
proof
let s be real number ; ::_thesis: ( s in proj1 .: S implies abs s < max ((abs ((p `1) - r)),(abs ((p `1) + r))) )
 proj1 .: S c= proj1 .: P by A2, RELAT_1:123;
hence  ( s in proj1 .: S implies abs s < max ((abs ((p `1) - r)),(abs ((p `1) + r))) ) by A7, JCT_MISC:3; ::_thesis: verum
end;
hence  proj1 .: S is real-bounded by A6, SEQ_4:4; ::_thesis: verum
end;

theorem :: JORDAN1C:4
for C1 being non empty compact Subset of (TOP-REAL 2)
for C2, S being non empty Subset of (TOP-REAL 2) st S = C1 \/ C2 & not proj1 .: C2 is empty & proj1 .: C2 is bounded_below holds
W-bound S = min ((W-bound C1),(W-bound C2))
proof
let C1 be non empty compact Subset of (TOP-REAL 2); ::_thesis: for C2, S being non empty Subset of (TOP-REAL 2) st S = C1 \/ C2 & not proj1 .: C2 is empty & proj1 .: C2 is bounded_below holds
W-bound S = min ((W-bound C1),(W-bound C2))
let C2, S be non empty Subset of (TOP-REAL 2); ::_thesis: ( S = C1 \/ C2 & not proj1 .: C2 is empty & proj1 .: C2 is bounded_below implies W-bound S = min ((W-bound C1),(W-bound C2)) )
assume that
A1: S = C1 \/ C2 and
A2: ( not proj1 .: C2 is empty & proj1 .: C2 is bounded_below ) ; ::_thesis: W-bound S = min ((W-bound C1),(W-bound C2))
set P1 = proj1 .: C1;
set P2 = proj1 .: C2;
set PS = proj1 .: S;
A3: W-bound C1 = lower_bound (proj1 .: C1) by SPRECT_1:43;
A4: W-bound C2 = lower_bound (proj1 .: C2) by SPRECT_1:43;
thus  W-bound S = lower_bound (proj1 .: S) by SPRECT_1:43
.= lower_bound ((proj1 .: C1) \/ (proj1 .: C2)) by A1, RELAT_1:120
.= min ((W-bound C1),(W-bound C2)) by A2, A3, A4, SEQ_4:142 ; ::_thesis: verum
end;

Lm7:  for p being Point of (TOP-REAL 2)
for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds
( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) )
proof
let p be Point of (TOP-REAL 2); ::_thesis: for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds
( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) )
set T = TOP-REAL 2;
let X be Subset of (TOP-REAL 2); ::_thesis: ( p in X & X is bounded implies ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) ) )
assume that
A1: p in X and
A2: X is bounded ; ::_thesis: ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) )
reconsider X = X as non empty Subset of (TOP-REAL 2) by A1;
A3: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:8;
A4: (proj1 | X) .: X = proj1 .: X by RELAT_1:129;
A5: proj1 .: X is real-bounded by A2, Th3;
then  (proj1 | X) .: X is bounded_below by A4, XXREAL_2:def_11;
then A6: proj1 | X is bounded_below by A3, MEASURE6:def_10;
 (proj1 | X) .: X is bounded_above by A4, A5, XXREAL_2:def_11;
then  proj1 | X is bounded_above by A3, MEASURE6:def_11;
then reconsider f = proj1 | X as bounded RealMap of ((TOP-REAL 2) | X) by A6;
reconsider p9 = p as Point of ((TOP-REAL 2) | X) by A1, PRE_TOPC:8;
A7: (proj1 | X) . p9 = p `1 by A1, PSCOMP_1:22;
then  lower_bound f <= p `1 by PSCOMP_1:1;
hence  ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) ) by A7, PSCOMP_1:4; ::_thesis: verum
end;

Lm8:  for p being Point of (TOP-REAL 2)
for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds
( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
proof
let p be Point of (TOP-REAL 2); ::_thesis: for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds
( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
set T = TOP-REAL 2;
let X be Subset of (TOP-REAL 2); ::_thesis: ( p in X & X is bounded implies ( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) ) )
assume that
A1: p in X and
A2: X is bounded ; ::_thesis: ( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
reconsider X = X as non empty Subset of (TOP-REAL 2) by A1;
A3: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:8;
A4: (proj2 | X) .: X = proj2 .: X by RELAT_1:129;
A5: proj2 .: X is real-bounded by A2, JCT_MISC:14;
then  (proj2 | X) .: X is bounded_below by A4, XXREAL_2:def_11;
then A6: proj2 | X is bounded_below by A3, MEASURE6:def_10;
 (proj2 | X) .: X is bounded_above by A4, A5, XXREAL_2:def_11;
then  proj2 | X is bounded_above by A3, MEASURE6:def_11;
then reconsider f = proj2 | X as bounded RealMap of ((TOP-REAL 2) | X) by A6;
reconsider p9 = p as Point of ((TOP-REAL 2) | X) by A1, PRE_TOPC:8;
A7: (proj2 | X) . p9 = p `2 by A1, PSCOMP_1:23;
then  lower_bound f <= p `2 by PSCOMP_1:1;
hence  ( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) ) by A7, PSCOMP_1:4; ::_thesis: verum
end;

theorem Th5: :: JORDAN1C:5
for p being Point of (TOP-REAL 2)
for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds
( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X )
proof
let p be Point of (TOP-REAL 2); ::_thesis: for X being Subset of (TOP-REAL 2) st p in X & X is bounded holds
( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X )
let X be Subset of (TOP-REAL 2); ::_thesis: ( p in X & X is bounded implies ( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X ) )
assume that
A1: p in X and
A2: X is bounded ; ::_thesis: ( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X )
 W-bound X = lower_bound (proj1 | X) by PSCOMP_1:def_7;
hence  W-bound X <= p `1 by A1, A2, Lm7; ::_thesis: ( p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X )
 E-bound X = upper_bound (proj1 | X) by PSCOMP_1:def_9;
hence  E-bound X >= p `1 by A1, A2, Lm7; ::_thesis: ( S-bound X <= p `2 & p `2 <= N-bound X )
 S-bound X = lower_bound (proj2 | X) by PSCOMP_1:def_10;
hence  S-bound X <= p `2 by A1, A2, Lm8; ::_thesis: p `2 <= N-bound X
 N-bound X = upper_bound (proj2 | X) by PSCOMP_1:def_8;
hence  p `2 <= N-bound X by A1, A2, Lm8; ::_thesis: verum
end;

Lm9:  for C being Subset of (TOP-REAL 2) st C is bounded holds
for h being real number st BDD C <> {} & h > W-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 >= h )
proof
let C be Subset of (TOP-REAL 2); ::_thesis: ( C is bounded implies for h being real number st BDD C <> {} & h > W-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 >= h ) )
assume A1: C is bounded ; ::_thesis: for h being real number st BDD C <> {} & h > W-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 >= h )
set X = proj1 | (BDD C);
let h be real number ; ::_thesis: ( BDD C <> {} & h > W-bound (BDD C) implies ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 >= h ) )
assume that
A2: BDD C <> {} and
A3: h > W-bound (BDD C) and
A4: for p being Point of (TOP-REAL 2) st p in BDD C holds
p `1 >= h ; ::_thesis: contradiction
reconsider T = (TOP-REAL 2) | (BDD C) as non empty TopSpace by A2;
 the carrier of T = BDD C by PRE_TOPC:8;
then  (proj1 | (BDD C)) .: the carrier of T = proj1 .: (BDD C) by RELAT_1:129;
then  (proj1 | (BDD C)) .: the carrier of T is real-bounded by A1, Th3, JORDAN2C:106;
then  (proj1 | (BDD C)) .: the carrier of T is bounded_below by XXREAL_2:def_11;
then reconsider X = proj1 | (BDD C) as bounded_below RealMap of T by MEASURE6:def_10;
A5: for p being Point of T holds X . p >= h
proof
let p be Point of T; ::_thesis: X . p >= h
A6: the carrier of T = BDD C by PRE_TOPC:8;
then  p in BDD C ;
then reconsider p9 = p as Point of (TOP-REAL 2) ;
 X . p = proj1 . p9 by A6, FUNCT_1:49;
then  X . p = p9 `1 by PSCOMP_1:def_5;
hence  X . p >= h by A4, A6; ::_thesis: verum
end;
A7: h is Real by XREAL_0:def_1;
 lower_bound X = W-bound (BDD C) by PSCOMP_1:def_7;
hence  contradiction by A3, A7, A5, PSCOMP_1:2; ::_thesis: verum
end;

Lm10:  for C being Subset of (TOP-REAL 2) st C is bounded holds
for h being real number st BDD C <> {} & h < E-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 <= h )
proof
let C be Subset of (TOP-REAL 2); ::_thesis: ( C is bounded implies for h being real number st BDD C <> {} & h < E-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 <= h ) )
assume A1: C is bounded ; ::_thesis: for h being real number st BDD C <> {} & h < E-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 <= h )
set X = proj1 | (BDD C);
let h be real number ; ::_thesis: ( BDD C <> {} & h < E-bound (BDD C) implies ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 <= h ) )
assume that
A2: BDD C <> {} and
A3: h < E-bound (BDD C) and
A4: for p being Point of (TOP-REAL 2) st p in BDD C holds
p `1 <= h ; ::_thesis: contradiction
reconsider T = (TOP-REAL 2) | (BDD C) as non empty TopSpace by A2;
 the carrier of T = BDD C by PRE_TOPC:8;
then  (proj1 | (BDD C)) .: the carrier of T = proj1 .: (BDD C) by RELAT_1:129;
then  (proj1 | (BDD C)) .: the carrier of T is real-bounded by A1, Th3, JORDAN2C:106;
then  (proj1 | (BDD C)) .: the carrier of T is bounded_above by XXREAL_2:def_11;
then reconsider X = proj1 | (BDD C) as bounded_above RealMap of T by MEASURE6:def_11;
A5: for p being Point of T holds X . p <= h
proof
let p be Point of T; ::_thesis: X . p <= h
A6: the carrier of T = BDD C by PRE_TOPC:8;
then  p in BDD C ;
then reconsider p9 = p as Point of (TOP-REAL 2) ;
 X . p = proj1 . p9 by A6, FUNCT_1:49;
then  X . p = p9 `1 by PSCOMP_1:def_5;
hence  X . p <= h by A4, A6; ::_thesis: verum
end;
 upper_bound X = E-bound (BDD C) by PSCOMP_1:def_9;
hence  contradiction by A3, A5, PSCOMP_1:5; ::_thesis: verum
end;

Lm11:  for C being Subset of (TOP-REAL 2) st C is bounded holds
for h being real number st BDD C <> {} & h < N-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 <= h )
proof
let C be Subset of (TOP-REAL 2); ::_thesis: ( C is bounded implies for h being real number st BDD C <> {} & h < N-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 <= h ) )
assume A1: C is bounded ; ::_thesis: for h being real number st BDD C <> {} & h < N-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 <= h )
set X = proj2 | (BDD C);
let h be real number ; ::_thesis: ( BDD C <> {} & h < N-bound (BDD C) implies ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 <= h ) )
assume that
A2: BDD C <> {} and
A3: h < N-bound (BDD C) and
A4: for p being Point of (TOP-REAL 2) st p in BDD C holds
p `2 <= h ; ::_thesis: contradiction
reconsider T = (TOP-REAL 2) | (BDD C) as non empty TopSpace by A2;
 the carrier of T = BDD C by PRE_TOPC:8;
then  (proj2 | (BDD C)) .: the carrier of T = proj2 .: (BDD C) by RELAT_1:129;
then  (proj2 | (BDD C)) .: the carrier of T is real-bounded by A1, JCT_MISC:14, JORDAN2C:106;
then  (proj2 | (BDD C)) .: the carrier of T is bounded_above by XXREAL_2:def_11;
then reconsider X = proj2 | (BDD C) as bounded_above RealMap of T by MEASURE6:def_11;
A5: for p being Point of T holds X . p <= h
proof
let p be Point of T; ::_thesis: X . p <= h
A6: the carrier of T = BDD C by PRE_TOPC:8;
then  p in BDD C ;
then reconsider p9 = p as Point of (TOP-REAL 2) ;
 X . p = proj2 . p9 by A6, FUNCT_1:49;
then  X . p = p9 `2 by PSCOMP_1:def_6;
hence  X . p <= h by A4, A6; ::_thesis: verum
end;
 upper_bound X = N-bound (BDD C) by PSCOMP_1:def_8;
hence  contradiction by A3, A5, PSCOMP_1:5; ::_thesis: verum
end;

Lm12:  for C being Subset of (TOP-REAL 2) st C is bounded holds
for h being real number st BDD C <> {} & h > S-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 >= h )
proof
let C be Subset of (TOP-REAL 2); ::_thesis: ( C is bounded implies for h being real number st BDD C <> {} & h > S-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 >= h ) )
assume A1: C is bounded ; ::_thesis: for h being real number st BDD C <> {} & h > S-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 >= h )
set X = proj2 | (BDD C);
let h be real number ; ::_thesis: ( BDD C <> {} & h > S-bound (BDD C) implies ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 >= h ) )
assume that
A2: BDD C <> {} and
A3: h > S-bound (BDD C) and
A4: for p being Point of (TOP-REAL 2) st p in BDD C holds
p `2 >= h ; ::_thesis: contradiction
reconsider T = (TOP-REAL 2) | (BDD C) as non empty TopSpace by A2;
 the carrier of T = BDD C by PRE_TOPC:8;
then  (proj2 | (BDD C)) .: the carrier of T = proj2 .: (BDD C) by RELAT_1:129;
then  (proj2 | (BDD C)) .: the carrier of T is real-bounded by A1, JCT_MISC:14, JORDAN2C:106;
then  (proj2 | (BDD C)) .: the carrier of T is bounded_below by XXREAL_2:def_11;
then reconsider X = proj2 | (BDD C) as bounded_below RealMap of T by MEASURE6:def_10;
A5: for p being Point of T holds X . p >= h
proof
let p be Point of T; ::_thesis: X . p >= h
A6: the carrier of T = BDD C by PRE_TOPC:8;
then  p in BDD C ;
then reconsider p9 = p as Point of (TOP-REAL 2) ;
 X . p = proj2 . p9 by A6, FUNCT_1:49;
then  X . p = p9 `2 by PSCOMP_1:def_6;
hence  X . p >= h by A4, A6; ::_thesis: verum
end;
A7: h is Real by XREAL_0:def_1;
 lower_bound X = S-bound (BDD C) by PSCOMP_1:def_10;
hence  contradiction by A3, A7, A5, PSCOMP_1:2; ::_thesis: verum
end;

Lm13: now__::_thesis:_for_C_being_Subset_of_(TOP-REAL_2)_st_C_is_bounded_holds_
not_UBD_C_is_empty
let C be Subset of (TOP-REAL 2); ::_thesis: ( C is bounded implies not UBD C is empty )
assume  C is bounded ; ::_thesis: not UBD C is empty
then  UBD C is_outside_component_of C by JORDAN2C:68;
hence  not UBD C is empty by JORDAN2C:def_3; ::_thesis: verum
end;

theorem Th6: :: JORDAN1C:6
for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds
W-bound C <= W-bound (BDD C)
proof
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( BDD C <> {} implies W-bound C <= W-bound (BDD C) )
set WC = W-bound C;
set WB = W-bound (BDD C);
set hal = ((W-bound (BDD C)) + (W-bound C)) / 2;
assume that
A1: BDD C <> {} and
A2: W-bound C > W-bound (BDD C) ; ::_thesis: contradiction
A3: ((W-bound (BDD C)) + (W-bound C)) / 2 < W-bound C by A2, XREAL_1:226;
now__::_thesis:_contradiction
percases ( for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `1 >= ((W-bound (BDD C)) + (W-bound C)) / 2 or ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `1 < ((W-bound (BDD C)) + (W-bound C)) / 2 ) ) ;
suppose for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `1 >= ((W-bound (BDD C)) + (W-bound C)) / 2 ; ::_thesis: contradiction
hence  contradiction by A1, A2, Lm9, XREAL_1:226; ::_thesis: verum
end;
suppose ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `1 < ((W-bound (BDD C)) + (W-bound C)) / 2 ) ; ::_thesis: contradiction
then consider q1 being Point of (TOP-REAL 2) such that
A4: q1 in BDD C and
A5: q1 `1 < ((W-bound (BDD C)) + (W-bound C)) / 2 ;
set Q = |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]|;
set WH = west_halfline |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]|;
A6: |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| `1 = ((W-bound C) + (q1 `1)) / 2 by EUCLID:52;
A7: q1 `1 < W-bound C by A3, A5, XXREAL_0:2;
 west_halfline |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| misses C
proof
A8: |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| `1 < W-bound C by A7, A6, XREAL_1:226;
assume  west_halfline |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| meets C ; ::_thesis: contradiction
then consider y being set  such that
A9: y in (west_halfline |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]|) /\ C by XBOOLE_0:4;
A10: y in C by A9, XBOOLE_0:def_4;
A11: y in west_halfline |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| by A9, XBOOLE_0:def_4;
reconsider y = y as Point of (TOP-REAL 2) by A9;
 y `1 <= |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| `1 by A11, TOPREAL1:def_13;
then  y `1 < W-bound C by A8, XXREAL_0:2;
hence  contradiction by A10, PSCOMP_1:24; ::_thesis: verum
end;
then A12: west_halfline |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| c= UBD C by JORDAN2C:126;
A13: q1 `2 = |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| `2 by EUCLID:52;
 q1 `1 < |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| `1 by A7, A6, XREAL_1:226;
then  q1 in west_halfline |[(((W-bound C) + (q1 `1)) / 2),(q1 `2)]| by A13, TOPREAL1:def_13;
then  q1 in (BDD C) /\ (UBD C) by A4, A12, XBOOLE_0:def_4;
then  BDD C meets UBD C by XBOOLE_0:def_7;
hence  contradiction by JORDAN2C:24; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem Th7: :: JORDAN1C:7
for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds
E-bound C >= E-bound (BDD C)
proof
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( BDD C <> {} implies E-bound C >= E-bound (BDD C) )
set WC = E-bound (BDD C);
set WB = E-bound C;
set hal = ((E-bound C) + (E-bound (BDD C))) / 2;
assume that
A1: BDD C <> {} and
A2: E-bound (BDD C) > E-bound C ; ::_thesis: contradiction
A3: ((E-bound C) + (E-bound (BDD C))) / 2 > E-bound C by A2, XREAL_1:226;
now__::_thesis:_contradiction
percases ( for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `1 <= ((E-bound C) + (E-bound (BDD C))) / 2 or ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `1 > ((E-bound C) + (E-bound (BDD C))) / 2 ) ) ;
suppose for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `1 <= ((E-bound C) + (E-bound (BDD C))) / 2 ; ::_thesis: contradiction
hence  contradiction by A1, A2, Lm10, XREAL_1:226; ::_thesis: verum
end;
suppose ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `1 > ((E-bound C) + (E-bound (BDD C))) / 2 ) ; ::_thesis: contradiction
then consider q1 being Point of (TOP-REAL 2) such that
A4: q1 in BDD C and
A5: q1 `1 > ((E-bound C) + (E-bound (BDD C))) / 2 ;
set Q = |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]|;
set WH = east_halfline |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]|;
A6: |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| `1 = ((E-bound C) + (q1 `1)) / 2 by EUCLID:52;
A7: q1 `1 > E-bound C by A3, A5, XXREAL_0:2;
 east_halfline |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| misses C
proof
A8: |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| `1 > E-bound C by A7, A6, XREAL_1:226;
assume  (east_halfline |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]|) /\ C <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider y being set  such that
A9: y in (east_halfline |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]|) /\ C by XBOOLE_0:def_1;
A10: y in C by A9, XBOOLE_0:def_4;
A11: y in east_halfline |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| by A9, XBOOLE_0:def_4;
reconsider y = y as Point of (TOP-REAL 2) by A9;
 y `1 >= |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| `1 by A11, TOPREAL1:def_11;
then  y `1 > E-bound C by A8, XXREAL_0:2;
hence  contradiction by A10, PSCOMP_1:24; ::_thesis: verum
end;
then A12: east_halfline |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| c= UBD C by JORDAN2C:127;
A13: q1 `2 = |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| `2 by EUCLID:52;
 q1 `1 > |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| `1 by A7, A6, XREAL_1:226;
then  q1 in east_halfline |[(((E-bound C) + (q1 `1)) / 2),(q1 `2)]| by A13, TOPREAL1:def_11;
then  q1 in (BDD C) /\ (UBD C) by A4, A12, XBOOLE_0:def_4;
then  BDD C meets UBD C by XBOOLE_0:4;
hence  contradiction by JORDAN2C:24; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem Th8: :: JORDAN1C:8
for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds
S-bound C <= S-bound (BDD C)
proof
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( BDD C <> {} implies S-bound C <= S-bound (BDD C) )
set WC = S-bound C;
set WB = S-bound (BDD C);
set hal = ((S-bound (BDD C)) + (S-bound C)) / 2;
assume that
A1: BDD C <> {} and
A2: S-bound C > S-bound (BDD C) ; ::_thesis: contradiction
A3: ((S-bound (BDD C)) + (S-bound C)) / 2 < S-bound C by A2, XREAL_1:226;
now__::_thesis:_contradiction
percases ( for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `2 >= ((S-bound (BDD C)) + (S-bound C)) / 2 or ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `2 < ((S-bound (BDD C)) + (S-bound C)) / 2 ) ) ;
suppose for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `2 >= ((S-bound (BDD C)) + (S-bound C)) / 2 ; ::_thesis: contradiction
hence  contradiction by A1, A2, Lm12, XREAL_1:226; ::_thesis: verum
end;
suppose ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `2 < ((S-bound (BDD C)) + (S-bound C)) / 2 ) ; ::_thesis: contradiction
then consider q1 being Point of (TOP-REAL 2) such that
A4: q1 in BDD C and
A5: q1 `2 < ((S-bound (BDD C)) + (S-bound C)) / 2 ;
set Q = |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]|;
set WH = south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]|;
A6: |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `2 = ((S-bound C) + (q1 `2)) / 2 by EUCLID:52;
A7: q1 `2 < S-bound C by A3, A5, XXREAL_0:2;
 south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| misses C
proof
A8: |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `2 < S-bound C by A7, A6, XREAL_1:226;
assume  (south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]|) /\ C <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider y being set  such that
A9: y in (south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]|) /\ C by XBOOLE_0:def_1;
A10: y in C by A9, XBOOLE_0:def_4;
A11: y in south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| by A9, XBOOLE_0:def_4;
reconsider y = y as Point of (TOP-REAL 2) by A9;
 y `2 <= |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `2 by A11, TOPREAL1:def_12;
then  y `2 < S-bound C by A8, XXREAL_0:2;
hence  contradiction by A10, PSCOMP_1:24; ::_thesis: verum
end;
then A12: south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| c= UBD C by JORDAN2C:128;
A13: q1 `1 = |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `1 by EUCLID:52;
 q1 `2 < |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| `2 by A7, A6, XREAL_1:226;
then  q1 in south_halfline |[(q1 `1),(((S-bound C) + (q1 `2)) / 2)]| by A13, TOPREAL1:def_12;
then  q1 in (BDD C) /\ (UBD C) by A4, A12, XBOOLE_0:def_4;
then  BDD C meets UBD C by XBOOLE_0:4;
hence  contradiction by JORDAN2C:24; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem Th9: :: JORDAN1C:9
for C being compact Subset of (TOP-REAL 2) st BDD C <> {} holds
N-bound C >= N-bound (BDD C)
proof
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( BDD C <> {} implies N-bound C >= N-bound (BDD C) )
set WC = N-bound (BDD C);
set WB = N-bound C;
set hal = ((N-bound C) + (N-bound (BDD C))) / 2;
assume that
A1: BDD C <> {} and
A2: N-bound (BDD C) > N-bound C ; ::_thesis: contradiction
A3: ((N-bound C) + (N-bound (BDD C))) / 2 > N-bound C by A2, XREAL_1:226;
now__::_thesis:_contradiction
percases ( for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `2 <= ((N-bound C) + (N-bound (BDD C))) / 2 or ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `2 > ((N-bound C) + (N-bound (BDD C))) / 2 ) ) ;
suppose for q1 being Point of (TOP-REAL 2) st q1 in BDD C holds
q1 `2 <= ((N-bound C) + (N-bound (BDD C))) / 2 ; ::_thesis: contradiction
hence  contradiction by A1, A2, Lm11, XREAL_1:226; ::_thesis: verum
end;
suppose ex q1 being Point of (TOP-REAL 2) st
( q1 in BDD C & q1 `2 > ((N-bound C) + (N-bound (BDD C))) / 2 ) ; ::_thesis: contradiction
then consider q1 being Point of (TOP-REAL 2) such that
A4: q1 in BDD C and
A5: q1 `2 > ((N-bound C) + (N-bound (BDD C))) / 2 ;
set Q = |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]|;
set WH = north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]|;
A6: |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| `2 = ((N-bound C) + (q1 `2)) / 2 by EUCLID:52;
A7: q1 `2 > N-bound C by A3, A5, XXREAL_0:2;
 north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| misses C
proof
A8: |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| `2 > N-bound C by A7, A6, XREAL_1:226;
assume  (north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]|) /\ C <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then consider y being set  such that
A9: y in (north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]|) /\ C by XBOOLE_0:def_1;
A10: y in C by A9, XBOOLE_0:def_4;
A11: y in north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| by A9, XBOOLE_0:def_4;
reconsider y = y as Point of (TOP-REAL 2) by A9;
 y `2 >= |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| `2 by A11, TOPREAL1:def_10;
then  y `2 > N-bound C by A8, XXREAL_0:2;
hence  contradiction by A10, PSCOMP_1:24; ::_thesis: verum
end;
then A12: north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| c= UBD C by JORDAN2C:129;
A13: q1 `1 = |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| `1 by EUCLID:52;
 q1 `2 > |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| `2 by A7, A6, XREAL_1:226;
then  q1 in north_halfline |[(q1 `1),(((N-bound C) + (q1 `2)) / 2)]| by A13, TOPREAL1:def_10;
then  q1 in (BDD C) /\ (UBD C) by A4, A12, XBOOLE_0:def_4;
then  BDD C meets UBD C by XBOOLE_0:4;
hence  contradiction by JORDAN2C:24; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem Th10: :: JORDAN1C:10
for n being Element of NAT
for p being Point of (TOP-REAL 2)
for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
1 < I
proof
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2)
for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
1 < I
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
1 < I
let C be compact non vertical Subset of (TOP-REAL 2); ::_thesis: for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
1 < I
set W = W-bound C;
set E = E-bound C;
set pW = (p `1) - (W-bound C);
set EW = (E-bound C) - (W-bound C);
let I be Integer; ::_thesis: ( p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] implies 1 < I )
assume that
A1: p in BDD C and
A2: I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] ; ::_thesis: 1 < I
A3: W-bound C <= W-bound (BDD C) by A1, Th6;
 BDD C is bounded by JORDAN2C:106;
then  p `1 >= W-bound (BDD C) by A1, Th5;
then  p `1 >= W-bound C by A3, XXREAL_0:2;
then A4: (p `1) - (W-bound C) >= 0 by XREAL_1:48;
set K = [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/];
 ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) - 1 < [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] by INT_1:def_6;
then A5: (((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) - 1) + 2 < [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] + 2 by XREAL_1:6;
 (E-bound C) - (W-bound C) > 0 by SPRECT_1:31, XREAL_1:50;
then  ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 1 >= 0 + 1 by A4, XREAL_1:6;
then  1 < [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] + 2 by A5, XXREAL_0:2;
hence  1 < I by A2, INT_1:28; ::_thesis: verum
end;

theorem Th11: :: JORDAN1C:11
for n being Element of NAT
for p being Point of (TOP-REAL 2)
for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))
proof
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2)
for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))
let C be compact non vertical Subset of (TOP-REAL 2); ::_thesis: for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))
set W = W-bound C;
set E = E-bound C;
set EW = (E-bound C) - (W-bound C);
set pW = (p `1) - (W-bound C);
let I be Integer; ::_thesis: ( p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] implies I + 1 <= len (Gauge (C,n)) )
assume that
A1: p in BDD C and
A2: I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] ; ::_thesis: I + 1 <= len (Gauge (C,n))
A3: E-bound C >= E-bound (BDD C) by A1, Th7;
 BDD C is bounded by JORDAN2C:106;
then  p `1 <= E-bound (BDD C) by A1, Th5;
then  p `1 <= E-bound C by A3, XXREAL_0:2;
then A4: (p `1) - (W-bound C) <= (E-bound C) - (W-bound C) by XREAL_1:9;
 (E-bound C) - (W-bound C) > 0 by SPRECT_1:31, XREAL_1:50;
then  ((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C)) <= 1 by A4, XREAL_1:185;
then  (((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n) <= 1 * (2 |^ n) by XREAL_1:64;
then A5: ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 3 <= (2 |^ n) + 3 by XREAL_1:7;
 I <= ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2 by A2, INT_1:def_6;
then A6: I + 1 <= (((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2) + 1 by XREAL_1:6;
 len (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN8:def_1;
hence  I + 1 <= len (Gauge (C,n)) by A5, A6, XXREAL_0:2; ::_thesis: verum
end;

theorem Th12: :: JORDAN1C:12
for n being Element of NAT
for p being Point of (TOP-REAL 2)
for C being compact non horizontal Subset of (TOP-REAL 2)
for J being Integer st p in BDD C & J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
( 1 < J & J + 1 <= width (Gauge (C,n)) )
proof
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2)
for C being compact non horizontal Subset of (TOP-REAL 2)
for J being Integer st p in BDD C & J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
( 1 < J & J + 1 <= width (Gauge (C,n)) )
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact non horizontal Subset of (TOP-REAL 2)
for J being Integer st p in BDD C & J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
( 1 < J & J + 1 <= width (Gauge (C,n)) )
let C be compact non horizontal Subset of (TOP-REAL 2); ::_thesis: for J being Integer st p in BDD C & J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
( 1 < J & J + 1 <= width (Gauge (C,n)) )
set W = S-bound C;
set E = N-bound C;
set EW = (N-bound C) - (S-bound C);
set pW = (p `2) - (S-bound C);
let I be Integer; ::_thesis: ( p in BDD C & I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] implies ( 1 < I & I + 1 <= width (Gauge (C,n)) ) )
assume that
A1: p in BDD C and
A2: I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] ; ::_thesis: ( 1 < I & I + 1 <= width (Gauge (C,n)) )
A3: (N-bound C) - (S-bound C) > 0 by SPRECT_1:32, XREAL_1:50;
set K = [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/];
 ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) - 1 < [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] by INT_1:def_6;
then A4: (((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) - 1) + 2 < [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] + 2 by XREAL_1:6;
A5: S-bound C <= S-bound (BDD C) by A1, Th8;
 BDD C is bounded by JORDAN2C:106;
then  p `2 >= S-bound (BDD C) by A1, Th5;
then  p `2 >= S-bound C by A5, XXREAL_0:2;
then  (p `2) - (S-bound C) >= 0 by XREAL_1:48;
then  ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 1 >= 0 + 1 by A3, XREAL_1:6;
then  1 < [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] + 2 by A4, XXREAL_0:2;
hence  1 < I by A2, INT_1:28; ::_thesis: I + 1 <= width (Gauge (C,n))
A6: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A7: N-bound C >= N-bound (BDD C) by A1, Th9;
 BDD C is bounded by JORDAN2C:106;
then  p `2 <= N-bound (BDD C) by A1, Th5;
then  p `2 <= N-bound C by A7, XXREAL_0:2;
then  (p `2) - (S-bound C) <= (N-bound C) - (S-bound C) by XREAL_1:9;
then  ((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C)) <= 1 by A3, XREAL_1:185;
then  (((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n) <= 1 * (2 |^ n) by XREAL_1:64;
then A8: ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 3 <= (2 |^ n) + 3 by XREAL_1:7;
 I <= ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2 by A2, INT_1:def_6;
then A9: I + 1 <= (((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2) + 1 by XREAL_1:6;
 len (Gauge (C,n)) = (2 |^ n) + 3 by JORDAN8:def_1;
hence  I + 1 <= width (Gauge (C,n)) by A6, A8, A9, XXREAL_0:2; ::_thesis: verum
end;

theorem Th13: :: JORDAN1C:13
for C being Simple_closed_curve
for n being Element of NAT
for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT
for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
let p be Point of (TOP-REAL 2); ::_thesis: for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
set W = W-bound C;
set EW = (E-bound C) - (W-bound C);
set PW = (p `1) - (W-bound C);
set KI = [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/];
let I be Integer; ::_thesis: ( I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] implies (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1 )
A1: (E-bound C) - (W-bound C) > 0 by TOPREAL5:17, XREAL_1:50;
 2 |^ n > 0 by NEWTON:83;
then A2: (((E-bound C) - (W-bound C)) / (2 |^ n)) * ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) = (p `1) - (W-bound C) by A1, Lm2;
assume  I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] ; ::_thesis: (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1
then A3: I - 2 = [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] by Lm1;
 [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] <= (((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n) by INT_1:def_6;
then A4: (((E-bound C) - (W-bound C)) / (2 |^ n)) * [\((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n))/] <= (((E-bound C) - (W-bound C)) / (2 |^ n)) * ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) by A1, XREAL_1:64;
 (W-bound C) + ((p `1) - (W-bound C)) = p `1 ;
hence  (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2)) <= p `1 by A3, A2, A4, XREAL_1:6; ::_thesis: verum
end;

theorem Th14: :: JORDAN1C:14
for C being Simple_closed_curve
for n being Element of NAT
for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT
for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2)
for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
let p be Point of (TOP-REAL 2); ::_thesis: for I being Integer st I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
set W = W-bound C;
set E = E-bound C;
set EW = (E-bound C) - (W-bound C);
set PW = (p `1) - (W-bound C);
let I be Integer; ::_thesis: ( I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] implies p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1)) )
set KI = I - 1;
A1: 2 |^ n > 0 by NEWTON:83;
assume  I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] ; ::_thesis: p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
then  I > (((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2) - 1 by INT_1:def_6;
then A2: I - 1 > (((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 1) - 1 by XREAL_1:9;
A3: (E-bound C) - (W-bound C) > 0 by TOPREAL5:17, XREAL_1:50;
then  ((E-bound C) - (W-bound C)) / (2 |^ n) > 0 by A1, XREAL_1:139;
then A4: (((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1) > (((E-bound C) - (W-bound C)) / (2 |^ n)) * ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) by A2, XREAL_1:68;
A5: (W-bound C) + ((p `1) - (W-bound C)) = p `1 ;
 (((E-bound C) - (W-bound C)) / (2 |^ n)) * ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) = (p `1) - (W-bound C) by A3, A1, Lm2;
hence  p `1 < (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1)) by A5, A4, XREAL_1:6; ::_thesis: verum
end;

theorem Th15: :: JORDAN1C:15
for C being Simple_closed_curve
for n being Element of NAT
for p being Point of (TOP-REAL 2)
for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) <= p `2
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT
for p being Point of (TOP-REAL 2)
for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) <= p `2
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2)
for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) <= p `2
let p be Point of (TOP-REAL 2); ::_thesis: for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)) <= p `2
set W = S-bound C;
set EW = (N-bound C) - (S-bound C);
set PW = (p `2) - (S-bound C);
set KI = [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/];
let I be Integer; ::_thesis: ( I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] implies (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 2)) <= p `2 )
A1: (N-bound C) - (S-bound C) > 0 by TOPREAL5:16, XREAL_1:50;
 2 |^ n > 0 by NEWTON:83;
then A2: (((N-bound C) - (S-bound C)) / (2 |^ n)) * ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) = (p `2) - (S-bound C) by A1, Lm2;
assume  I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] ; ::_thesis: (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 2)) <= p `2
then A3: I - 2 = [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] by Lm1;
 [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] <= (((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n) by INT_1:def_6;
then A4: (((N-bound C) - (S-bound C)) / (2 |^ n)) * [\((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n))/] <= (((N-bound C) - (S-bound C)) / (2 |^ n)) * ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) by A1, XREAL_1:64;
 (S-bound C) + ((p `2) - (S-bound C)) = p `2 ;
hence  (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 2)) <= p `2 by A3, A2, A4, XREAL_1:6; ::_thesis: verum
end;

theorem Th16: :: JORDAN1C:16
for C being Simple_closed_curve
for n being Element of NAT
for p being Point of (TOP-REAL 2)
for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1))
proof
let C be Simple_closed_curve; ::_thesis: for n being Element of NAT
for p being Point of (TOP-REAL 2)
for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1))
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL 2)
for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1))
let p be Point of (TOP-REAL 2); ::_thesis: for J being Integer st J = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] holds
p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1))
set W = S-bound C;
set E = N-bound C;
set EW = (N-bound C) - (S-bound C);
set PW = (p `2) - (S-bound C);
let I be Integer; ::_thesis: ( I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] implies p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 1)) )
set KI = I - 1;
A1: 2 |^ n > 0 by NEWTON:83;
assume  I = [\(((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] ; ::_thesis: p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 1))
then  I > (((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2) - 1 by INT_1:def_6;
then A2: I - 1 > (((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 1) - 1 by XREAL_1:9;
A3: (S-bound C) + ((p `2) - (S-bound C)) = p `2 ;
A4: (N-bound C) - (S-bound C) > 0 by TOPREAL5:16, XREAL_1:50;
then A5: ((N-bound C) - (S-bound C)) / (2 |^ n) > 0 by A1, XREAL_1:139;
 (((N-bound C) - (S-bound C)) / (2 |^ n)) * ((((p `2) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) = (p `2) - (S-bound C) by A4, A1, Lm2;
then  (((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 1) > (p `2) - (S-bound C) by A2, A5, XREAL_1:68;
hence  p `2 < (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (I - 1)) by A3, XREAL_1:6; ::_thesis: verum
end;

theorem Th17: :: JORDAN1C:17
for C being closed Subset of (TOP-REAL 2)
for p being Point of (Euclid 2) st p in BDD C holds
ex r being Real st
( r > 0 & Ball (p,r) c= BDD C )
proof
let C be closed Subset of (TOP-REAL 2); ::_thesis: for p being Point of (Euclid 2) st p in BDD C holds
ex r being Real st
( r > 0 & Ball (p,r) c= BDD C )
let p be Point of (Euclid 2); ::_thesis: ( p in BDD C implies ex r being Real st
( r > 0 & Ball (p,r) c= BDD C ) )
set W = Int (BDD C);
assume  p in BDD C ; ::_thesis: ex r being Real st
( r > 0 & Ball (p,r) c= BDD C )
then  p in Int (BDD C) by TOPS_1:23;
then consider r being real number  such that
A1: r > 0 and
A2: Ball (p,r) c= BDD C by GOBOARD6:5;
reconsider r = r as Real by XREAL_0:def_1;
take  r ; ::_thesis: ( r > 0 & Ball (p,r) c= BDD C )
thus  ( r > 0 & Ball (p,r) c= BDD C ) by A1, A2; ::_thesis: verum
end;

theorem :: JORDAN1C:18
for C being Simple_closed_curve
for n, i, j being Element of NAT
for p, q being Point of (TOP-REAL 2)
for r being real number st dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r & p in cell ((Gauge (C,n)),i,j) & q in cell ((Gauge (C,n)),i,j) & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
dist (p,q) < 2 * r
proof
let C be Simple_closed_curve; ::_thesis: for n, i, j being Element of NAT
for p, q being Point of (TOP-REAL 2)
for r being real number st dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r & p in cell ((Gauge (C,n)),i,j) & q in cell ((Gauge (C,n)),i,j) & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
dist (p,q) < 2 * r
let n, i, j be Element of NAT ; ::_thesis: for p, q being Point of (TOP-REAL 2)
for r being real number st dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r & p in cell ((Gauge (C,n)),i,j) & q in cell ((Gauge (C,n)),i,j) & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
dist (p,q) < 2 * r
set G = Gauge (C,n);
let p, q be Point of (TOP-REAL 2); ::_thesis: for r being real number st dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r & p in cell ((Gauge (C,n)),i,j) & q in cell ((Gauge (C,n)),i,j) & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds
dist (p,q) < 2 * r
let r be real number ; ::_thesis: ( dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r & p in cell ((Gauge (C,n)),i,j) & q in cell ((Gauge (C,n)),i,j) & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) implies dist (p,q) < 2 * r )
assume that
A1: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r and
A2: dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < r and
A3: p in cell ((Gauge (C,n)),i,j) and
A4: q in cell ((Gauge (C,n)),i,j) and
A5: 1 <= i and
A6: i + 1 <= len (Gauge (C,n)) and
A7: 1 <= j and
A8: j + 1 <= width (Gauge (C,n)) ; ::_thesis: dist (p,q) < 2 * r
A9: p `1 <= ((Gauge (C,n)) * ((i + 1),j)) `1 by A3, A5, A6, A7, A8, JORDAN9:17;
A10: p `2 <= ((Gauge (C,n)) * (i,(j + 1))) `2 by A3, A5, A6, A7, A8, JORDAN9:17;
A11: ((Gauge (C,n)) * (i,j)) `2 <= p `2 by A3, A5, A6, A7, A8, JORDAN9:17;
 j <= j + 1 by NAT_1:11;
then A12: j <= width (Gauge (C,n)) by A8, XXREAL_0:2;
 i <= i + 1 by NAT_1:11;
then A13: i <= len (Gauge (C,n)) by A6, XXREAL_0:2;
then A14: [i,j] in Indices (Gauge (C,n)) by A5, A7, A12, MATRIX_1:36;
A15: q `2 <= ((Gauge (C,n)) * (i,(j + 1))) `2 by A4, A5, A6, A7, A8, JORDAN9:17;
A16: ((Gauge (C,n)) * (i,j)) `2 <= q `2 by A4, A5, A6, A7, A8, JORDAN9:17;
A17: q `1 <= ((Gauge (C,n)) * ((i + 1),j)) `1 by A4, A5, A6, A7, A8, JORDAN9:17;
A18: ((Gauge (C,n)) * (i,j)) `1 <= q `1 by A4, A5, A6, A7, A8, JORDAN9:17;
 1 <= j + 1 by NAT_1:11;
then  [i,(j + 1)] in Indices (Gauge (C,n)) by A5, A8, A13, MATRIX_1:36;
then A19: (((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2) < r by A1, A14, Th2;
 1 <= i + 1 by NAT_1:11;
then  [(i + 1),j] in Indices (Gauge (C,n)) by A6, A7, A12, MATRIX_1:36;
then  (((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1) < r by A2, A14, Th1;
then A20: ((((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1)) + ((((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2)) < r + r by A19, XREAL_1:8;
 ((Gauge (C,n)) * (i,j)) `1 <= p `1 by A3, A5, A6, A7, A8, JORDAN9:17;
then  dist (p,q) <= ((((Gauge (C,n)) * ((i + 1),j)) `1) - (((Gauge (C,n)) * (i,j)) `1)) + ((((Gauge (C,n)) * (i,(j + 1))) `2) - (((Gauge (C,n)) * (i,j)) `2)) by A9, A11, A10, A18, A17, A16, A15, TOPREAL6:95;
hence  dist (p,q) < 2 * r by A20, XXREAL_0:2; ::_thesis: verum
end;

theorem :: JORDAN1C:19
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `2 <> N-bound (BDD C)
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `2 <> N-bound (BDD C)
reconsider P = p as Point of (Euclid 2) by Lm3;
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies p `2 <> N-bound (BDD C) )
A1: BDD C is bounded by JORDAN2C:106;
assume  p in BDD C ; ::_thesis: p `2 <> N-bound (BDD C)
then consider r being Real such that
A2: r > 0 and
A3: Ball (P,r) c= BDD C by Th17;
set EX = |[(p `1),((p `2) + (r / 2))]|;
 0 < r / 2 by A2, XREAL_1:139;
then A4: (p `2) + (r / 2) > (p `2) + 0 by XREAL_1:6;
assume A5: p `2 = N-bound (BDD C) ; ::_thesis: contradiction
A6: not |[(p `1),((p `2) + (r / 2))]| in BDD C
proof
assume  |[(p `1),((p `2) + (r / 2))]| in BDD C ; ::_thesis: contradiction
then  |[(p `1),((p `2) + (r / 2))]| `2 <= N-bound (BDD C) by A1, Th5;
hence  contradiction by A5, A4, EUCLID:52; ::_thesis: verum
end;
A7: P = |[(p `1),(p `2)]| by EUCLID:53;
 r / 2 < r by A2, XREAL_1:216;
then  |[(p `1),((p `2) + (r / 2))]| in Ball (P,r) by A2, A7, GOBOARD6:8;
hence  contradiction by A3, A6; ::_thesis: verum
end;

theorem :: JORDAN1C:20
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `1 <> E-bound (BDD C)
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `1 <> E-bound (BDD C)
reconsider P = p as Point of (Euclid 2) by Lm3;
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies p `1 <> E-bound (BDD C) )
A1: BDD C is bounded by JORDAN2C:106;
assume  p in BDD C ; ::_thesis: p `1 <> E-bound (BDD C)
then consider r being Real such that
A2: r > 0 and
A3: Ball (P,r) c= BDD C by Th17;
set EX = |[((p `1) + (r / 2)),(p `2)]|;
 0 < r / 2 by A2, XREAL_1:139;
then A4: (p `1) + (r / 2) > (p `1) + 0 by XREAL_1:6;
assume A5: p `1 = E-bound (BDD C) ; ::_thesis: contradiction
A6: not |[((p `1) + (r / 2)),(p `2)]| in BDD C
proof
assume  |[((p `1) + (r / 2)),(p `2)]| in BDD C ; ::_thesis: contradiction
then  |[((p `1) + (r / 2)),(p `2)]| `1 <= E-bound (BDD C) by A1, Th5;
hence  contradiction by A5, A4, EUCLID:52; ::_thesis: verum
end;
A7: P = |[(p `1),(p `2)]| by EUCLID:53;
 r / 2 < r by A2, XREAL_1:216;
then  |[((p `1) + (r / 2)),(p `2)]| in Ball (P,r) by A2, A7, GOBOARD6:7;
hence  contradiction by A3, A6; ::_thesis: verum
end;

theorem :: JORDAN1C:21
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `2 <> S-bound (BDD C)
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `2 <> S-bound (BDD C)
reconsider P = p as Point of (Euclid 2) by Lm3;
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies p `2 <> S-bound (BDD C) )
A1: BDD C is bounded by JORDAN2C:106;
assume  p in BDD C ; ::_thesis: p `2 <> S-bound (BDD C)
then consider r being Real such that
A2: r > 0 and
A3: Ball (P,r) c= BDD C by Th17;
set EX = |[(p `1),((p `2) - (r / 2))]|;
 0 < r / 2 by A2, XREAL_1:139;
then  (p `2) + (r / 2) > (p `2) + 0 by XREAL_1:6;
then A4: (p `2) - (r / 2) < p `2 by XREAL_1:19;
assume A5: p `2 = S-bound (BDD C) ; ::_thesis: contradiction
A6: not |[(p `1),((p `2) - (r / 2))]| in BDD C
proof
assume  |[(p `1),((p `2) - (r / 2))]| in BDD C ; ::_thesis: contradiction
then  |[(p `1),((p `2) - (r / 2))]| `2 >= S-bound (BDD C) by A1, Th5;
hence  contradiction by A5, A4, EUCLID:52; ::_thesis: verum
end;
A7: P = |[(p `1),(p `2)]| by EUCLID:53;
 r / 2 < r by A2, XREAL_1:216;
then  |[(p `1),((p `2) - (r / 2))]| in Ball (P,r) by A2, A7, GOBOARD6:10;
hence  contradiction by A3, A6; ::_thesis: verum
end;

theorem Th22: :: JORDAN1C:22
for p being Point of (TOP-REAL 2)
for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `1 <> W-bound (BDD C)
proof
let p be Point of (TOP-REAL 2); ::_thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `1 <> W-bound (BDD C)
reconsider P = p as Point of (Euclid 2) by Lm3;
let C be compact Subset of (TOP-REAL 2); ::_thesis: ( p in BDD C implies p `1 <> W-bound (BDD C) )
A1: BDD C is bounded by JORDAN2C:106;
assume  p in BDD C ; ::_thesis: p `1 <> W-bound (BDD C)
then consider r being Real such that
A2: r > 0 and
A3: Ball (P,r) c= BDD C by Th17;
set EX = |[((p `1) - (r / 2)),(p `2)]|;
 0 < r / 2 by A2, XREAL_1:139;
then  (p `1) + (r / 2) > (p `1) + 0 by XREAL_1:6;
then A4: (p `1) - (r / 2) < p `1 by XREAL_1:19;
assume A5: p `1 = W-bound (BDD C) ; ::_thesis: contradiction
A6: not |[((p `1) - (r / 2)),(p `2)]| in BDD C
proof
assume  |[((p `1) - (r / 2)),(p `2)]| in BDD C ; ::_thesis: contradiction
then  |[((p `1) - (r / 2)),(p `2)]| `1 >= W-bound (BDD C) by A1, Th5;
hence  contradiction by A5, A4, EUCLID:52; ::_thesis: verum
end;
A7: P = |[(p `1),(p `2)]| by EUCLID:53;
 r / 2 < r by A2, XREAL_1:216;
then  |[((p `1) - (r / 2)),(p `2)]| in Ball (P,r) by A2, A7, GOBOARD6:9;
hence  contradiction by A3, A6; ::_thesis: verum
end;

theorem :: JORDAN1C:23
for C being Simple_closed_curve
for p being Point of (TOP-REAL 2) st p in BDD C holds
ex n, i, j being Element of 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 )
proof
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 Element of 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 Element of 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 Element of 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 Element of 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 Element of 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_1:36;
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_1:36;
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_1:36;
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;
percases ( p `1 <> ((Gauge (C,n)) * (I,J)) `1 or p `1 = ((Gauge (C,n)) * (I,J)) `1 ) ;
supposeA22: p `1 <> ((Gauge (C,n)) * (I,J)) `1 ; ::_thesis: ex i, j being Element of 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 )
take  I ; ::_thesis: ex j being Element of 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 )
take  J ; ::_thesis: ( 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 )
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: ( 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 )
 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, XBOOLE_1:1; ::_thesis: verum
end;
supposeA23: p `1 = ((Gauge (C,n)) * (I,J)) `1 ; ::_thesis: ex i, j being Element of 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 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: ex j being Element of NAT st
( 1 < I -' 1 & I -' 1 < len (Gauge (C,n)) & 1 < j & j < width (Gauge (C,n)) & 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 )
take  J ; ::_thesis: ( 1 < I -' 1 & I -' 1 < len (Gauge (C,n)) & 1 < J & J < width (Gauge (C,n)) & 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 )
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: contradiction
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: verum
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: ( 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 )
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, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;

theorem :: JORDAN1C:24
for C being Subset of (TOP-REAL 2) st C is bounded holds
not UBD C is empty by Lm13;