:: by Artur Korni{\l}owicz, Robert Milewski, Adam Naumowicz and

::

:: Received September 12, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

3 = (2 * 1) + 1

;

then Lm1: 3 div 2 = 1

by NAT_D:def 1;

1 = (2 * 0) + 1

;

then Lm2: 1 div 2 = 0

by NAT_D:def 1;

:: deftheorem defines Center JORDAN1A:def 1 :

for f being FinSequence holds Center f = ((len f) div 2) + 1;

for f being FinSequence holds Center f = ((len f) div 2) + 1;

registration

ex b_{1} being Subset of (TOP-REAL 2) st

( b_{1} is compact & not b_{1} is vertical & not b_{1} is horizontal & b_{1} is being_simple_closed_curve & not b_{1} is empty )
end;

cluster non empty being_simple_closed_curve compact non horizontal non vertical for Element of K16( the U1 of (TOP-REAL 2));

existence ex b

( b

proof end;

theorem Th3: :: JORDAN1A:3

for D being non empty Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in N-most D holds

p `2 = N-bound D

for p being Point of (TOP-REAL 2) st p in N-most D holds

p `2 = N-bound D

proof end;

theorem Th4: :: JORDAN1A:4

for D being non empty Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in E-most D holds

p `1 = E-bound D

for p being Point of (TOP-REAL 2) st p in E-most D holds

p `1 = E-bound D

proof end;

theorem Th5: :: JORDAN1A:5

for D being non empty Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in S-most D holds

p `2 = S-bound D

for p being Point of (TOP-REAL 2) st p in S-most D holds

p `2 = S-bound D

proof end;

theorem Th6: :: JORDAN1A:6

for D being non empty Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in W-most D holds

p `1 = W-bound D

for p being Point of (TOP-REAL 2) st p in W-most D holds

p `1 = W-bound D

proof end;

theorem :: JORDAN1A:11

for p, q being Point of (TOP-REAL 2)

for r being Real st p `1 = q `1 & r in [.(proj2 . p),(proj2 . q).] holds

|[(p `1),r]| in LSeg (p,q)

for r being Real st p `1 = q `1 & r in [.(proj2 . p),(proj2 . q).] holds

|[(p `1),r]| in LSeg (p,q)

proof end;

theorem :: JORDAN1A:12

for p, q being Point of (TOP-REAL 2)

for r being Real st p `2 = q `2 & r in [.(proj1 . p),(proj1 . q).] holds

|[r,(p `2)]| in LSeg (p,q)

for r being Real st p `2 = q `2 & r in [.(proj1 . p),(proj1 . q).] holds

|[r,(p `2)]| in LSeg (p,q)

proof end;

theorem :: JORDAN1A:13

for p, q being Point of (TOP-REAL 2)

for s being Real st p in Vertical_Line s & q in Vertical_Line s holds

LSeg (p,q) c= Vertical_Line s

for s being Real st p in Vertical_Line s & q in Vertical_Line s holds

LSeg (p,q) c= Vertical_Line s

proof end;

theorem :: JORDAN1A:15

for s being Real

for A, B being Subset of (TOP-REAL 2) st A misses B & A c= Vertical_Line s & B c= Vertical_Line s holds

proj2 .: A misses proj2 .: B

for A, B being Subset of (TOP-REAL 2) st A misses B & A c= Vertical_Line s & B c= Vertical_Line s holds

proj2 .: A misses proj2 .: B

proof end;

theorem :: JORDAN1A:16

for i, j being Nat

for G being Go-board st 1 <= i & i <= len G & 1 <= j & j <= width G holds

G * (i,j) in LSeg ((G * (i,1)),(G * (i,(width G))))

for G being Go-board st 1 <= i & i <= len G & 1 <= j & j <= width G holds

G * (i,j) in LSeg ((G * (i,1)),(G * (i,(width G))))

proof end;

theorem :: JORDAN1A:17

for i, j being Nat

for G being Go-board st 1 <= i & i <= len G & 1 <= j & j <= width G holds

G * (i,j) in LSeg ((G * (1,j)),(G * ((len G),j)))

for G being Go-board st 1 <= i & i <= len G & 1 <= j & j <= width G holds

G * (i,j) in LSeg ((G * (1,j)),(G * ((len G),j)))

proof end;

theorem Th18: :: JORDAN1A:18

for i1, i2, j1, j2 being Nat

for G being Go-board st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 <= i2 & i2 <= len G holds

(G * (i1,j1)) `1 <= (G * (i2,j2)) `1

for G being Go-board st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 <= i2 & i2 <= len G holds

(G * (i1,j1)) `1 <= (G * (i2,j2)) `1

proof end;

theorem Th19: :: JORDAN1A:19

for i1, i2, j1, j2 being Nat

for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= j2 & j2 <= width G holds

(G * (i1,j1)) `2 <= (G * (i2,j2)) `2

for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= j2 & j2 <= width G holds

(G * (i1,j1)) `2 <= (G * (i2,j2)) `2

proof end;

theorem Th20: :: JORDAN1A:20

for t being Nat

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds

(G * (t,(width G))) `2 >= N-bound (L~ f)

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds

(G * (t,(width G))) `2 >= N-bound (L~ f)

proof end;

theorem Th21: :: JORDAN1A:21

for t being Nat

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds

(G * (1,t)) `1 <= W-bound (L~ f)

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds

(G * (1,t)) `1 <= W-bound (L~ f)

proof end;

theorem Th22: :: JORDAN1A:22

for t being Nat

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds

(G * (t,1)) `2 <= S-bound (L~ f)

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= len G holds

(G * (t,1)) `2 <= S-bound (L~ f)

proof end;

theorem Th23: :: JORDAN1A:23

for t being Nat

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds

(G * ((len G),t)) `1 >= E-bound (L~ f)

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds

(G * ((len G),t)) `1 >= E-bound (L~ f)

proof end;

theorem Th24: :: JORDAN1A:24

for i, j being Nat

for G being Go-board st i <= len G & j <= width G holds

not cell (G,i,j) is empty

for G being Go-board st i <= len G & j <= width G holds

not cell (G,i,j) is empty

proof end;

theorem Th25: :: JORDAN1A:25

for i, j being Nat

for G being Go-board st i <= len G & j <= width G holds

cell (G,i,j) is connected

for G being Go-board st i <= len G & j <= width G holds

cell (G,i,j) is connected

proof end;

theorem :: JORDAN1A:28

for n being Nat

for D being non empty Subset of (TOP-REAL 2) holds width (Gauge (D,n)) = (2 |^ n) + 3

for D being non empty Subset of (TOP-REAL 2) holds width (Gauge (D,n)) = (2 |^ n) + 3

proof end;

theorem :: JORDAN1A:29

for i, j being Nat

for D being non empty Subset of (TOP-REAL 2) st i < j holds

len (Gauge (D,i)) < len (Gauge (D,j))

for D being non empty Subset of (TOP-REAL 2) st i < j holds

len (Gauge (D,i)) < len (Gauge (D,j))

proof end;

theorem :: JORDAN1A:30

for i, j being Nat

for D being non empty Subset of (TOP-REAL 2) st i <= j holds

len (Gauge (D,i)) <= len (Gauge (D,j))

for D being non empty Subset of (TOP-REAL 2) st i <= j holds

len (Gauge (D,i)) <= len (Gauge (D,j))

proof end;

theorem Th31: :: JORDAN1A:31

for i, m, n being Nat

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < len (Gauge (D,m)) holds

( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < len (Gauge (D,n)) )

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < len (Gauge (D,m)) holds

( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < len (Gauge (D,n)) )

proof end;

theorem Th32: :: JORDAN1A:32

for i, m, n being Nat

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < width (Gauge (D,m)) holds

( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < width (Gauge (D,n)) )

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < width (Gauge (D,m)) holds

( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < width (Gauge (D,n)) )

proof end;

theorem Th33: :: JORDAN1A:33

for i, j, m, n being Nat

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < len (Gauge (D,m)) & 1 < j & j < width (Gauge (D,m)) holds

for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds

(Gauge (D,m)) * (i,j) = (Gauge (D,n)) * (i1,j1)

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < len (Gauge (D,m)) & 1 < j & j < width (Gauge (D,m)) holds

for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds

(Gauge (D,m)) * (i,j) = (Gauge (D,n)) * (i1,j1)

proof end;

theorem Th34: :: JORDAN1A:34

for i, m, n being Nat

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < len (Gauge (D,m)) holds

( 1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (i - 1)) + 2 <= len (Gauge (D,n)) )

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < len (Gauge (D,m)) holds

( 1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (i - 1)) + 2 <= len (Gauge (D,n)) )

proof end;

theorem Th35: :: JORDAN1A:35

for i, m, n being Nat

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < width (Gauge (D,m)) holds

( 1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (i - 1)) + 2 <= width (Gauge (D,n)) )

for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < width (Gauge (D,m)) holds

( 1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (i - 1)) + 2 <= width (Gauge (D,n)) )

proof end;

Lm3: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n being Nat holds

( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )

for n being Nat holds

( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n being Nat holds

( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )

let n be Nat; :: thesis: ( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )

set G = Gauge (D,n);

0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 by XREAL_1:6;

hence 1 <= Center (Gauge (D,n)) ; :: thesis: Center (Gauge (D,n)) <= len (Gauge (D,n))

0 < len (Gauge (D,n)) by JORDAN8:10;

then (len (Gauge (D,n))) div 2 < len (Gauge (D,n)) by INT_1:56;

hence Center (Gauge (D,n)) <= len (Gauge (D,n)) by NAT_1:13; :: thesis: verum

end;
( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )

let n be Nat; :: thesis: ( 1 <= Center (Gauge (D,n)) & Center (Gauge (D,n)) <= len (Gauge (D,n)) )

set G = Gauge (D,n);

0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 by XREAL_1:6;

hence 1 <= Center (Gauge (D,n)) ; :: thesis: Center (Gauge (D,n)) <= len (Gauge (D,n))

0 < len (Gauge (D,n)) by JORDAN8:10;

then (len (Gauge (D,n))) div 2 < len (Gauge (D,n)) by INT_1:56;

hence Center (Gauge (D,n)) <= len (Gauge (D,n)) by NAT_1:13; :: thesis: verum

Lm4: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds

[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))

for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds

[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds

[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))

let n, j be Nat; :: thesis: ( 1 <= j & j <= len (Gauge (D,n)) implies [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) )

set G = Gauge (D,n);

assume A1: ( 1 <= j & j <= len (Gauge (D,n)) ) ; :: thesis: [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))

A2: ( len (Gauge (D,n)) = width (Gauge (D,n)) & 0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 ) by JORDAN8:def 1, XREAL_1:6;

Center (Gauge (D,n)) <= len (Gauge (D,n)) by Lm3;

hence [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) by A1, A2, MATRIX_0:30; :: thesis: verum

end;
[(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))

let n, j be Nat; :: thesis: ( 1 <= j & j <= len (Gauge (D,n)) implies [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) )

set G = Gauge (D,n);

assume A1: ( 1 <= j & j <= len (Gauge (D,n)) ) ; :: thesis: [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n))

A2: ( len (Gauge (D,n)) = width (Gauge (D,n)) & 0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 ) by JORDAN8:def 1, XREAL_1:6;

Center (Gauge (D,n)) <= len (Gauge (D,n)) by Lm3;

hence [(Center (Gauge (D,n))),j] in Indices (Gauge (D,n)) by A1, A2, MATRIX_0:30; :: thesis: verum

Lm5: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds

[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))

for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds

[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n, j being Nat st 1 <= j & j <= len (Gauge (D,n)) holds

[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))

let n, j be Nat; :: thesis: ( 1 <= j & j <= len (Gauge (D,n)) implies [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) )

set G = Gauge (D,n);

assume A1: ( 1 <= j & j <= len (Gauge (D,n)) ) ; :: thesis: [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))

A2: ( len (Gauge (D,n)) = width (Gauge (D,n)) & 0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 ) by JORDAN8:def 1, XREAL_1:6;

Center (Gauge (D,n)) <= len (Gauge (D,n)) by Lm3;

hence [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) by A1, A2, MATRIX_0:30; :: thesis: verum

end;
[j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))

let n, j be Nat; :: thesis: ( 1 <= j & j <= len (Gauge (D,n)) implies [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) )

set G = Gauge (D,n);

assume A1: ( 1 <= j & j <= len (Gauge (D,n)) ) ; :: thesis: [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n))

A2: ( len (Gauge (D,n)) = width (Gauge (D,n)) & 0 + 1 <= ((len (Gauge (D,n))) div 2) + 1 ) by JORDAN8:def 1, XREAL_1:6;

Center (Gauge (D,n)) <= len (Gauge (D,n)) by Lm3;

hence [j,(Center (Gauge (D,n)))] in Indices (Gauge (D,n)) by A1, A2, MATRIX_0:30; :: thesis: verum

Lm6: for n being Nat

for D being non empty Subset of (TOP-REAL 2)

for w being Real st n > 0 holds

(w / (2 |^ n)) * ((Center (Gauge (D,n))) - 2) = w / 2

proof end;

Lm7: now :: thesis: for m, n being Nat

for c, d being Real st 0 <= c & m <= n holds

c / (2 |^ n) <= c / (2 |^ m)

for c, d being Real st 0 <= c & m <= n holds

c / (2 |^ n) <= c / (2 |^ m)

let m, n be Nat; :: thesis: for c, d being Real st 0 <= c & m <= n holds

c / (2 |^ n) <= c / (2 |^ m)

let c, d be Real; :: thesis: ( 0 <= c & m <= n implies c / (2 |^ n) <= c / (2 |^ m) )

assume A1: 0 <= c ; :: thesis: ( m <= n implies c / (2 |^ n) <= c / (2 |^ m) )

assume m <= n ; :: thesis: c / (2 |^ n) <= c / (2 |^ m)

then ( 0 < 2 |^ m & 2 |^ m <= 2 |^ n ) by NEWTON:83, PREPOWER:93;

hence c / (2 |^ n) <= c / (2 |^ m) by A1, XREAL_1:118; :: thesis: verum

end;
c / (2 |^ n) <= c / (2 |^ m)

let c, d be Real; :: thesis: ( 0 <= c & m <= n implies c / (2 |^ n) <= c / (2 |^ m) )

assume A1: 0 <= c ; :: thesis: ( m <= n implies c / (2 |^ n) <= c / (2 |^ m) )

assume m <= n ; :: thesis: c / (2 |^ n) <= c / (2 |^ m)

then ( 0 < 2 |^ m & 2 |^ m <= 2 |^ n ) by NEWTON:83, PREPOWER:93;

hence c / (2 |^ n) <= c / (2 |^ m) by A1, XREAL_1:118; :: thesis: verum

Lm8: for m, n being Nat

for c, d being Real st 0 <= c & m <= n holds

d + (c / (2 |^ n)) <= d + (c / (2 |^ m))

by XREAL_1:6, Lm7;

Lm9: now :: thesis: for m, n being Nat

for c, d being Real st 0 <= c & m <= n holds

d - (c / (2 |^ m)) <= d - (c / (2 |^ n))

for c, d being Real st 0 <= c & m <= n holds

d - (c / (2 |^ m)) <= d - (c / (2 |^ n))

let m, n be Nat; :: thesis: for c, d being Real st 0 <= c & m <= n holds

d - (c / (2 |^ m)) <= d - (c / (2 |^ n))

let c, d be Real; :: thesis: ( 0 <= c & m <= n implies d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) )

assume ( 0 <= c & m <= n ) ; :: thesis: d - (c / (2 |^ m)) <= d - (c / (2 |^ n))

then c / (2 |^ n) <= c / (2 |^ m) by Lm7;

hence d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) by XREAL_1:13; :: thesis: verum

end;
d - (c / (2 |^ m)) <= d - (c / (2 |^ n))

let c, d be Real; :: thesis: ( 0 <= c & m <= n implies d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) )

assume ( 0 <= c & m <= n ) ; :: thesis: d - (c / (2 |^ m)) <= d - (c / (2 |^ n))

then c / (2 |^ n) <= c / (2 |^ m) by Lm7;

hence d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) by XREAL_1:13; :: thesis: verum

theorem Th36: :: JORDAN1A:36

for i, j, m, n being Nat

for D being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (D,n)) & 1 <= j & j <= len (Gauge (D,m)) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) holds

((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1

for D being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (D,n)) & 1 <= j & j <= len (Gauge (D,m)) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) holds

((Gauge (D,n)) * ((Center (Gauge (D,n))),i)) `1 = ((Gauge (D,m)) * ((Center (Gauge (D,m))),j)) `1

proof end;

theorem :: JORDAN1A:37

for i, j, m, n being Nat

for D being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (D,n)) & 1 <= j & j <= len (Gauge (D,m)) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) holds

((Gauge (D,n)) * (i,(Center (Gauge (D,n))))) `2 = ((Gauge (D,m)) * (j,(Center (Gauge (D,m))))) `2

for D being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (D,n)) & 1 <= j & j <= len (Gauge (D,m)) & ( ( n > 0 & m > 0 ) or ( n = 0 & m = 0 ) ) holds

((Gauge (D,n)) * (i,(Center (Gauge (D,n))))) `2 = ((Gauge (D,m)) * (j,(Center (Gauge (D,m))))) `2

proof end;

Lm10: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n being Nat

for e, w being Real holds w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n))

for n being Nat

for e, w being Real holds w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n))

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n being Nat

for e, w being Real holds w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n))

let n be Nat; :: thesis: for e, w being Real holds w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n))

let e, w be Real; :: thesis: w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n))

A1: 2 |^ n <> 0 by NEWTON:83;

thus w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = w + (((e - w) / (2 |^ n)) * (((2 |^ n) + 3) - 2)) by JORDAN8:def 1

.= (w + (((e - w) / (2 |^ n)) * (2 |^ n))) + ((e - w) / (2 |^ n))

.= (w + (e - w)) + ((e - w) / (2 |^ n)) by A1, XCMPLX_1:87

.= e + ((e - w) / (2 |^ n)) ; :: thesis: verum

end;
for e, w being Real holds w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n))

let n be Nat; :: thesis: for e, w being Real holds w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n))

let e, w be Real; :: thesis: w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = e + ((e - w) / (2 |^ n))

A1: 2 |^ n <> 0 by NEWTON:83;

thus w + (((e - w) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) = w + (((e - w) / (2 |^ n)) * (((2 |^ n) + 3) - 2)) by JORDAN8:def 1

.= (w + (((e - w) / (2 |^ n)) * (2 |^ n))) + ((e - w) / (2 |^ n))

.= (w + (e - w)) + ((e - w) / (2 |^ n)) by A1, XCMPLX_1:87

.= e + ((e - w) / (2 |^ n)) ; :: thesis: verum

Lm11: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n, i being Nat st [i,1] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))

for n, i being Nat st [i,1] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n, i being Nat st [i,1] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))

let n, i be Nat; :: thesis: ( [i,1] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [i,1] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))

hence ((Gauge (D,n)) * (i,1)) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (1 - 2)))]| `2 by JORDAN8:def 1

.= (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) by EUCLID:52 ;

:: thesis: verum

end;
((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))

let n, i be Nat; :: thesis: ( [i,1] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [i,1] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * (i,1)) `2 = (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n))

hence ((Gauge (D,n)) * (i,1)) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (1 - 2)))]| `2 by JORDAN8:def 1

.= (S-bound D) - (((N-bound D) - (S-bound D)) / (2 |^ n)) by EUCLID:52 ;

:: thesis: verum

Lm12: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n, i being Nat st [1,i] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))

for n, i being Nat st [1,i] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n, i being Nat st [1,i] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))

let n, i be Nat; :: thesis: ( [1,i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [1,i] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))

hence ((Gauge (D,n)) * (1,i)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1 by JORDAN8:def 1

.= (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) by EUCLID:52 ;

:: thesis: verum

end;
((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))

let n, i be Nat; :: thesis: ( [1,i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [1,i] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * (1,i)) `1 = (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n))

hence ((Gauge (D,n)) * (1,i)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (1 - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1 by JORDAN8:def 1

.= (W-bound D) - (((E-bound D) - (W-bound D)) / (2 |^ n)) by EUCLID:52 ;

:: thesis: verum

Lm13: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n, i being Nat st [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))

for n, i being Nat st [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n, i being Nat st [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))

let n, i be Nat; :: thesis: ( [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))

hence ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)))]| `2 by JORDAN8:def 1

.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) by EUCLID:52

.= (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) by Lm10 ;

:: thesis: verum

end;
((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))

let n, i be Nat; :: thesis: ( [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [i,(len (Gauge (D,n)))] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n))

hence ((Gauge (D,n)) * (i,(len (Gauge (D,n))))) `2 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * (i - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)))]| `2 by JORDAN8:def 1

.= (S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) by EUCLID:52

.= (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) by Lm10 ;

:: thesis: verum

Lm14: now :: thesis: for D being non empty Subset of (TOP-REAL 2)

for n, i being Nat st [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))

for n, i being Nat st [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))

let D be non empty Subset of (TOP-REAL 2); :: thesis: for n, i being Nat st [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) holds

((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))

let n, i be Nat; :: thesis: ( [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))

hence ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1 by JORDAN8:def 1

.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) by EUCLID:52

.= (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) by Lm10 ;

:: thesis: verum

end;
((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))

let n, i be Nat; :: thesis: ( [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) implies ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) )

set a = N-bound D;

set s = S-bound D;

set w = W-bound D;

set e = E-bound D;

set G = Gauge (D,n);

assume [(len (Gauge (D,n))),i] in Indices (Gauge (D,n)) ; :: thesis: ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n))

hence ((Gauge (D,n)) * ((len (Gauge (D,n))),i)) `1 = |[((W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2))),((S-bound D) + ((((N-bound D) - (S-bound D)) / (2 |^ n)) * (i - 2)))]| `1 by JORDAN8:def 1

.= (W-bound D) + ((((E-bound D) - (W-bound D)) / (2 |^ n)) * ((len (Gauge (D,n))) - 2)) by EUCLID:52

.= (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) by Lm10 ;

:: thesis: verum

theorem :: JORDAN1A:38

for i being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,1)) holds

((Gauge (C,1)) * ((Center (Gauge (C,1))),i)) `1 = ((W-bound C) + (E-bound C)) / 2

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,1)) holds

((Gauge (C,1)) * ((Center (Gauge (C,1))),i)) `1 = ((W-bound C) + (E-bound C)) / 2

proof end;

theorem :: JORDAN1A:39

for i being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,1)) holds

((Gauge (C,1)) * (i,(Center (Gauge (C,1))))) `2 = ((S-bound C) + (N-bound C)) / 2

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,1)) holds

((Gauge (C,1)) * (i,(Center (Gauge (C,1))))) `2 = ((S-bound C) + (N-bound C)) / 2

proof end;

theorem Th40: :: JORDAN1A:40

for i, j, m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds

((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds

((Gauge (E,n)) * (i,(len (Gauge (E,n))))) `2 <= ((Gauge (E,m)) * (j,(len (Gauge (E,m))))) `2

proof end;

theorem :: JORDAN1A:41

for i, j, m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds

((Gauge (E,n)) * ((len (Gauge (E,n))),i)) `1 <= ((Gauge (E,m)) * ((len (Gauge (E,m))),j)) `1

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds

((Gauge (E,n)) * ((len (Gauge (E,n))),i)) `1 <= ((Gauge (E,m)) * ((len (Gauge (E,m))),j)) `1

proof end;

theorem :: JORDAN1A:42

for i, j, m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds

((Gauge (E,m)) * (1,j)) `1 <= ((Gauge (E,n)) * (1,i)) `1

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds

((Gauge (E,m)) * (1,j)) `1 <= ((Gauge (E,n)) * (1,i)) `1

proof end;

theorem :: JORDAN1A:43

for i, j, m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds

((Gauge (E,m)) * (j,1)) `2 <= ((Gauge (E,n)) * (i,1)) `2

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (E,n)) & 1 <= j & j <= len (Gauge (E,m)) & m <= n holds

((Gauge (E,m)) * (j,1)) `2 <= ((Gauge (E,n)) * (i,1)) `2

proof end;

theorem :: JORDAN1A:44

for m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n holds

LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n)))))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n holds

LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),(len (Gauge (E,n)))))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))

proof end;

theorem :: JORDAN1A:45

for j, m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

LSeg (((Gauge (E,n)) * ((Center (Gauge (E,n))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j)))

proof end;

theorem :: JORDAN1A:46

for j, m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= m & m <= n & 1 <= j & j <= width (Gauge (E,n)) holds

LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,n)) * ((Center (Gauge (E,n))),j))) c= LSeg (((Gauge (E,m)) * ((Center (Gauge (E,m))),1)),((Gauge (E,m)) * ((Center (Gauge (E,m))),(len (Gauge (E,m))))))

proof end;

theorem Th47: :: JORDAN1A:47

for i, j, m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) holds

for i1, j1 being Nat st ((2 |^ (n -' m)) * (i - 2)) + 2 <= i1 & i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (j - 2)) + 2 <= j1 & j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 holds

cell ((Gauge (E,n)),i1,j1) c= cell ((Gauge (E,m)),i,j)

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 < i & i + 1 < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) holds

for i1, j1 being Nat st ((2 |^ (n -' m)) * (i - 2)) + 2 <= i1 & i1 < ((2 |^ (n -' m)) * (i - 1)) + 2 & ((2 |^ (n -' m)) * (j - 2)) + 2 <= j1 & j1 < ((2 |^ (n -' m)) * (j - 1)) + 2 holds

cell ((Gauge (E,n)),i1,j1) c= cell ((Gauge (E,m)),i,j)

proof end;

theorem :: JORDAN1A:48

for i, j, m, n being Nat

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 3 <= i & i < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) holds

for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds

cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j)

for E being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 3 <= i & i < len (Gauge (E,m)) & 1 < j & j + 1 < width (Gauge (E,m)) holds

for i1, j1 being Nat st i1 = ((2 |^ (n -' m)) * (i - 2)) + 2 & j1 = ((2 |^ (n -' m)) * (j - 2)) + 2 holds

cell ((Gauge (E,n)),(i1 -' 1),j1) c= cell ((Gauge (E,m)),(i -' 1),j)

proof end;

theorem :: JORDAN1A:49

for i, n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge (C,n)) holds

cell ((Gauge (C,n)),i,0) c= UBD C

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge (C,n)) holds

cell ((Gauge (C,n)),i,0) c= UBD C

proof end;

theorem :: JORDAN1A:50

for i, n being Nat

for E, C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge (E,n)) holds

cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= UBD E

for E, C being compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge (E,n)) holds

cell ((Gauge (E,n)),i,(width (Gauge (E,n)))) c= UBD E

proof end;

theorem Th51: :: JORDAN1A:51

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in C holds

north_halfline p meets L~ (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in C holds

north_halfline p meets L~ (Cage (C,n))

proof end;

theorem Th52: :: JORDAN1A:52

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in C holds

east_halfline p meets L~ (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in C holds

east_halfline p meets L~ (Cage (C,n))

proof end;

theorem Th53: :: JORDAN1A:53

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in C holds

south_halfline p meets L~ (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in C holds

south_halfline p meets L~ (Cage (C,n))

proof end;

theorem Th54: :: JORDAN1A:54

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in C holds

west_halfline p meets L~ (Cage (C,n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in C holds

west_halfline p meets L~ (Cage (C,n))

proof end;

Lm15: for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) )

proof end;

Lm16: for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) )

proof end;

Lm17: for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) )

proof end;

theorem Th55: :: JORDAN1A:55

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) )

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) )

proof end;

theorem Th56: :: JORDAN1A:56

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) )

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) )

proof end;

theorem Th57: :: JORDAN1A:57

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) )

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex k, t being Nat st

( 1 <= k & k < len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) )

proof end;

theorem Th58: :: JORDAN1A:58

for k, n, t being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,(width (Gauge (C,n)))) holds

(Cage (C,n)) /. k in N-most (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,(width (Gauge (C,n)))) holds

(Cage (C,n)) /. k in N-most (L~ (Cage (C,n)))

proof end;

theorem Th59: :: JORDAN1A:59

for k, n, t being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) holds

(Cage (C,n)) /. k in W-most (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (1,t) holds

(Cage (C,n)) /. k in W-most (L~ (Cage (C,n)))

proof end;

theorem Th60: :: JORDAN1A:60

for k, n, t being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) holds

(Cage (C,n)) /. k in S-most (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= len (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * (t,1) holds

(Cage (C,n)) /. k in S-most (L~ (Cage (C,n)))

proof end;

theorem Th61: :: JORDAN1A:61

for k, n, t being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) holds

(Cage (C,n)) /. k in E-most (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= k & k <= len (Cage (C,n)) & 1 <= t & t <= width (Gauge (C,n)) & (Cage (C,n)) /. k = (Gauge (C,n)) * ((len (Gauge (C,n))),t) holds

(Cage (C,n)) /. k in E-most (L~ (Cage (C,n)))

proof end;

theorem Th62: :: JORDAN1A:62

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-bound (L~ (Cage (C,n))) = (W-bound C) - (((E-bound C) - (W-bound C)) / (2 |^ n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds W-bound (L~ (Cage (C,n))) = (W-bound C) - (((E-bound C) - (W-bound C)) / (2 |^ n))

proof end;

theorem Th63: :: JORDAN1A:63

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-bound (L~ (Cage (C,n))) = (S-bound C) - (((N-bound C) - (S-bound C)) / (2 |^ n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds S-bound (L~ (Cage (C,n))) = (S-bound C) - (((N-bound C) - (S-bound C)) / (2 |^ n))

proof end;

theorem Th64: :: JORDAN1A:64

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound (L~ (Cage (C,n))) = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds E-bound (L~ (Cage (C,n))) = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n))

proof end;

theorem :: JORDAN1A:65

for m, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-bound (L~ (Cage (C,n)))) + (S-bound (L~ (Cage (C,n)))) = (N-bound (L~ (Cage (C,m)))) + (S-bound (L~ (Cage (C,m))))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-bound (L~ (Cage (C,n)))) + (S-bound (L~ (Cage (C,n)))) = (N-bound (L~ (Cage (C,m)))) + (S-bound (L~ (Cage (C,m))))

proof end;

theorem :: JORDAN1A:66

for m, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n)))) = (E-bound (L~ (Cage (C,m)))) + (W-bound (L~ (Cage (C,m))))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-bound (L~ (Cage (C,n)))) + (W-bound (L~ (Cage (C,n)))) = (E-bound (L~ (Cage (C,m)))) + (W-bound (L~ (Cage (C,m))))

proof end;

theorem :: JORDAN1A:67

for i, j being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds

E-bound (L~ (Cage (C,j))) < E-bound (L~ (Cage (C,i)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds

E-bound (L~ (Cage (C,j))) < E-bound (L~ (Cage (C,i)))

proof end;

theorem :: JORDAN1A:68

for i, j being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds

W-bound (L~ (Cage (C,i))) < W-bound (L~ (Cage (C,j)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds

W-bound (L~ (Cage (C,i))) < W-bound (L~ (Cage (C,j)))

proof end;

theorem :: JORDAN1A:69

for i, j being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds

S-bound (L~ (Cage (C,i))) < S-bound (L~ (Cage (C,j)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st i < j holds

S-bound (L~ (Cage (C,i))) < S-bound (L~ (Cage (C,j)))

proof end;

theorem :: JORDAN1A:70

for i, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds

N-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,(len (Gauge (C,n))))) `2

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds

N-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,(len (Gauge (C,n))))) `2

proof end;

theorem :: JORDAN1A:71

for i, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds

E-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * ((len (Gauge (C,n))),i)) `1

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds

E-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * ((len (Gauge (C,n))),i)) `1

proof end;

theorem :: JORDAN1A:72

for i, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds

S-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,1)) `2

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds

S-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (i,1)) `2

proof end;

theorem :: JORDAN1A:73

for i, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds

W-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (1,i)) `1

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge (C,n)) holds

W-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * (1,i)) `1

proof end;

theorem Th74: :: JORDAN1A:74

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in C & p in (north_halfline x) /\ (L~ (Cage (C,n))) holds

p `2 > x `2

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in C & p in (north_halfline x) /\ (L~ (Cage (C,n))) holds

p `2 > x `2

proof end;

theorem Th75: :: JORDAN1A:75

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in C & p in (east_halfline x) /\ (L~ (Cage (C,n))) holds

p `1 > x `1

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in C & p in (east_halfline x) /\ (L~ (Cage (C,n))) holds

p `1 > x `1

proof end;

theorem Th76: :: JORDAN1A:76

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in C & p in (south_halfline x) /\ (L~ (Cage (C,n))) holds

p `2 < x `2

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in C & p in (south_halfline x) /\ (L~ (Cage (C,n))) holds

p `2 < x `2

proof end;

theorem Th77: :: JORDAN1A:77

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in C & p in (west_halfline x) /\ (L~ (Cage (C,n))) holds

p `1 < x `1

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in C & p in (west_halfline x) /\ (L~ (Cage (C,n))) holds

p `1 < x `1

proof end;

theorem Th78: :: JORDAN1A:78

for i, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in N-most C & p in north_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds

LSeg ((Cage (C,n)),i) is horizontal

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in N-most C & p in north_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds

LSeg ((Cage (C,n)),i) is horizontal

proof end;

theorem Th79: :: JORDAN1A:79

for i, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds

LSeg ((Cage (C,n)),i) is vertical

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in E-most C & p in east_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds

LSeg ((Cage (C,n)),i) is vertical

proof end;

theorem Th80: :: JORDAN1A:80

for i, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in S-most C & p in south_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds

LSeg ((Cage (C,n)),i) is horizontal

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in S-most C & p in south_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds

LSeg ((Cage (C,n)),i) is horizontal

proof end;

theorem Th81: :: JORDAN1A:81

for i, n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in W-most C & p in west_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds

LSeg ((Cage (C,n)),i) is vertical

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in W-most C & p in west_halfline x & 1 <= i & i < len (Cage (C,n)) & p in LSeg ((Cage (C,n)),i) holds

LSeg ((Cage (C,n)),i) is vertical

proof end;

theorem Th82: :: JORDAN1A:82

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in N-most C & p in (north_halfline x) /\ (L~ (Cage (C,n))) holds

p `2 = N-bound (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in N-most C & p in (north_halfline x) /\ (L~ (Cage (C,n))) holds

p `2 = N-bound (L~ (Cage (C,n)))

proof end;

theorem Th83: :: JORDAN1A:83

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in E-most C & p in (east_halfline x) /\ (L~ (Cage (C,n))) holds

p `1 = E-bound (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in E-most C & p in (east_halfline x) /\ (L~ (Cage (C,n))) holds

p `1 = E-bound (L~ (Cage (C,n)))

proof end;

theorem Th84: :: JORDAN1A:84

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in S-most C & p in (south_halfline x) /\ (L~ (Cage (C,n))) holds

p `2 = S-bound (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in S-most C & p in (south_halfline x) /\ (L~ (Cage (C,n))) holds

p `2 = S-bound (L~ (Cage (C,n)))

proof end;

theorem Th85: :: JORDAN1A:85

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in W-most C & p in (west_halfline x) /\ (L~ (Cage (C,n))) holds

p `1 = W-bound (L~ (Cage (C,n)))

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for p, x being Point of (TOP-REAL 2) st x in W-most C & p in (west_halfline x) /\ (L~ (Cage (C,n))) holds

p `1 = W-bound (L~ (Cage (C,n)))

proof end;

theorem :: JORDAN1A:86

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for x being Point of (TOP-REAL 2) st x in N-most C holds

ex p being Point of (TOP-REAL 2) st (north_halfline x) /\ (L~ (Cage (C,n))) = {p}

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for x being Point of (TOP-REAL 2) st x in N-most C holds

ex p being Point of (TOP-REAL 2) st (north_halfline x) /\ (L~ (Cage (C,n))) = {p}

proof end;

theorem :: JORDAN1A:87

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for x being Point of (TOP-REAL 2) st x in E-most C holds

ex p being Point of (TOP-REAL 2) st (east_halfline x) /\ (L~ (Cage (C,n))) = {p}

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for x being Point of (TOP-REAL 2) st x in E-most C holds

ex p being Point of (TOP-REAL 2) st (east_halfline x) /\ (L~ (Cage (C,n))) = {p}

proof end;

theorem :: JORDAN1A:88

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for x being Point of (TOP-REAL 2) st x in S-most C holds

ex p being Point of (TOP-REAL 2) st (south_halfline x) /\ (L~ (Cage (C,n))) = {p}

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for x being Point of (TOP-REAL 2) st x in S-most C holds

ex p being Point of (TOP-REAL 2) st (south_halfline x) /\ (L~ (Cage (C,n))) = {p}

proof end;

theorem :: JORDAN1A:89

for n being Nat

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for x being Point of (TOP-REAL 2) st x in W-most C holds

ex p being Point of (TOP-REAL 2) st (west_halfline x) /\ (L~ (Cage (C,n))) = {p}

for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)

for x being Point of (TOP-REAL 2) st x in W-most C holds

ex p being Point of (TOP-REAL 2) st (west_halfline x) /\ (L~ (Cage (C,n))) = {p}

proof end;