:: JORDAN1A semantic presentation

3 = (2 * 1) + 1
;

then Lm1: 3 div 2 = 1
by NAT_1:def 1;

1 = (2 * 0) + 1
;

then Lm2: 1 div 2 = 0
by NAT_1:def 1;

Lm3: for s1, s3, s4, l being real number st s1 <= s3 & s1 <= s4 & 0 <= l & l <= 1 holds
s1 <= ((1 - l) * s3) + (l * s4)
by XREAL_1:175;

Lm4: for s1, s3, s4, l being real number st s3 <= s1 & s4 <= s1 & 0 <= l & l <= 1 holds
((1 - l) * s3) + (l * s4) <= s1
by XREAL_1:176;

theorem :: JORDAN1A:1

canceled;

theorem :: JORDAN1A:2

canceled;

theorem :: JORDAN1A:3

canceled;

theorem Th4: :: JORDAN1A:4

for i, j being natural number st j > 0 & i mod j = 0 holds
i div j = i / j

proof end;

theorem Th5: :: JORDAN1A:5

for i, n being natural number st n > 0 holds
(i |^ n) div i = (i |^ n) / i

proof end;

theorem Th6: :: JORDAN1A:6

for r being real number
for n being natural number st 0 < n & 1 < r holds
1 < r |^ n

proof end;

theorem Th7: :: JORDAN1A:7

for r being real number
for m, n being natural number st r > 1 & m > n holds
r |^ m > r |^ n

proof end;

theorem Th8: :: JORDAN1A:8

for T being non empty TopSpace
for A, B, C being Subset of T st A is connected & C is_a_component_of B & A meets C & A c= B holds
A c= C

proof end;

definition

let f be FinSequence;
func Center f -> Nat equals :: JORDAN1A:def 1
((len f) div 2) + 1;
coherence ;

end;

:: deftheorem defines Center JORDAN1A:def 1 :

theorem :: JORDAN1A:9

for f being FinSequence st not len f is even holds
len f = (2 * (Center f)) - 1

proof end;

theorem :: JORDAN1A:10

for f being FinSequence st len f is even holds
len f = (2 * (Center f)) - 2

proof end;

registration

cluster non empty compact non horizontal non vertical being_simple_closed_curve Element of K40(the carrier of (TOP-REAL 2));
existence

proof end;

cluster non empty compact horizontal Element of K40(the carrier of (TOP-REAL 2));
existence

proof end;

cluster non empty compact vertical Element of K40(the carrier of (TOP-REAL 2));
existence

proof end;

end;

theorem Th11: :: JORDAN1A:11

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

proof end;

theorem Th12: :: JORDAN1A:12

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

proof end;

theorem Th13: :: JORDAN1A:13

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

proof end;

theorem Th14: :: JORDAN1A:14

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

proof end;

theorem :: JORDAN1A:15

for D being Subset of (TOP-REAL 2) holds BDD D misses D

proof end;

theorem :: JORDAN1A:16

for S being non empty being_simple_closed_curve Subset of (TOP-REAL 2) holds
( Lower_Arc S c= S & Upper_Arc S c= S )

proof end;

theorem Th17: :: JORDAN1A:17

for p being Point of (TOP-REAL 2) holds p in Vertical_Line (p `1 )

proof end;

theorem :: JORDAN1A:18

for r, s being real number holds |[r,s]| in Vertical_Line r

proof end;

theorem :: JORDAN1A:19

for s being real number
for A being Subset of (TOP-REAL 2) st A c= Vertical_Line s holds
A is vertical

proof end;

theorem :: JORDAN1A:20

for r, s being real number holds
( proj2 . |[r,s]| = s & proj1 . |[r,s]| = r )

proof end;

theorem :: JORDAN1A:21

for p, q being Point of (TOP-REAL 2)
for r being real number st p `1 = q `1 & r in [.(proj2 . p),(proj2 . q).] holds
|[(p `1 ),r]| in LSeg p,q

proof end;

theorem :: JORDAN1A:22

for p, q being Point of (TOP-REAL 2)
for r being real number st p `2 = q `2 & r in [.(proj1 . p),(proj1 . q).] holds
|[r,(p `2 )]| in LSeg p,q

proof end;

theorem :: JORDAN1A:23

for p, q being Point of (TOP-REAL 2)
for s being real number st p in Vertical_Line s & q in Vertical_Line s holds
LSeg p,q c= Vertical_Line s

proof end;

registration

let S be non empty being_simple_closed_curve Subset of (TOP-REAL 2);
cluster Lower_Arc S -> compact ;
coherence

proof end;

cluster Upper_Arc S -> compact ;
coherence

proof end;

end;

theorem :: JORDAN1A:24

for A, B being Subset of (TOP-REAL 2) st A meets B holds
proj2 .: A meets proj2 .: B

proof end;

theorem :: JORDAN1A:25

for s being real number
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 Th26: :: JORDAN1A:26

for S being closed Subset of (TOP-REAL 2) st S is Bounded holds
proj2 .: S is closed

proof end;

theorem Th27: :: JORDAN1A:27

for S being Subset of (TOP-REAL 2) st S is Bounded holds
proj2 .: S is bounded

proof end;

theorem :: JORDAN1A:28

for S being compact Subset of (TOP-REAL 2) holds proj2 .: S is compact

proof end;

scheme :: JORDAN1A:sch 1
TRSubsetEx{ F₁() -> Nat, P₁[ set ] } :

ex A being Subset of (TOP-REAL F₁()) st
for p being Point of (TOP-REAL F₁()) holds
( p in A iff P₁[p] )

proof end;

scheme :: JORDAN1A:sch 2
TRSubsetUniq{ F₁() -> Nat, P₁[ set ] } :

for A, B being Subset of (TOP-REAL F₁()) st ( for p being Point of (TOP-REAL F₁()) holds
( p in A iff P₁[p] ) ) & ( for p being Point of (TOP-REAL F₁()) holds
( p in B iff P₁[p] ) ) holds
A = B

proof end;

definition

let p be Point of (TOP-REAL 2);
func north_halfline p -> Subset of (TOP-REAL 2) means :Def2: :: JORDAN1A:def 2
for x being Point of (TOP-REAL 2) holds
( x in it iff ( x `1 = p `1 & x `2 >= p `2 ) );
existence

proof end;

uniqueness

proof end;

func east_halfline p -> Subset of (TOP-REAL 2) means :Def3: :: JORDAN1A:def 3
for x being Point of (TOP-REAL 2) holds
( x in it iff ( x `1 >= p `1 & x `2 = p `2 ) );
existence

proof end;

uniqueness

proof end;

func south_halfline p -> Subset of (TOP-REAL 2) means :Def4: :: JORDAN1A:def 4
for x being Point of (TOP-REAL 2) holds
( x in it iff ( x `1 = p `1 & x `2 <= p `2 ) );
existence

proof end;

uniqueness

proof end;

func west_halfline p -> Subset of (TOP-REAL 2) means :Def5: :: JORDAN1A:def 5
for x being Point of (TOP-REAL 2) holds
( x in it iff ( x `1 <= p `1 & x `2 = p `2 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines north_halfline JORDAN1A:def 2 :

:: deftheorem Def3 defines east_halfline JORDAN1A:def 3 :

:: deftheorem Def4 defines south_halfline JORDAN1A:def 4 :

:: deftheorem Def5 defines west_halfline JORDAN1A:def 5 :

theorem Th29: :: JORDAN1A:29

for p being Point of (TOP-REAL 2) holds north_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 >= p `2 ) }

proof end;

theorem Th30: :: JORDAN1A:30

for p being Point of (TOP-REAL 2) holds north_halfline p = { |[(p `1 ),r]| where r is Element of REAL : r >= p `2 }

proof end;

theorem Th31: :: JORDAN1A:31

for p being Point of (TOP-REAL 2) holds east_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 >= p `1 & q `2 = p `2 ) }

proof end;

theorem Th32: :: JORDAN1A:32

for p being Point of (TOP-REAL 2) holds east_halfline p = { |[r,(p `2 )]| where r is Element of REAL : r >= p `1 }

proof end;

theorem Th33: :: JORDAN1A:33

for p being Point of (TOP-REAL 2) holds south_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 = p `1 & q `2 <= p `2 ) }

proof end;

theorem Th34: :: JORDAN1A:34

for p being Point of (TOP-REAL 2) holds south_halfline p = { |[(p `1 ),r]| where r is Element of REAL : r <= p `2 }

proof end;

theorem Th35: :: JORDAN1A:35

for p being Point of (TOP-REAL 2) holds west_halfline p = { q where q is Point of (TOP-REAL 2) : ( q `1 <= p `1 & q `2 = p `2 ) }

proof end;

theorem Th36: :: JORDAN1A:36

for p being Point of (TOP-REAL 2) holds west_halfline p = { |[r,(p `2 )]| where r is Element of REAL : r <= p `1 }

proof end;

Lm5: for x0, y0 being real number
for P being Subset of (TOP-REAL 2) st P = { |[x,y0]| where x is Real : x <= x0 } holds
P is convex

proof end;

Lm6: for x0, y0 being real number
for P being Subset of (TOP-REAL 2) st P = { |[x0,y]| where y is Real : y <= y0 } holds
P is convex

proof end;

Lm7: for x0, y0 being real number
for P being Subset of (TOP-REAL 2) st P = { |[x,y0]| where x is Real : x >= x0 } holds
P is convex

proof end;

Lm8: for x0, y0 being real number
for P being Subset of (TOP-REAL 2) st P = { |[x0,y]| where y is Real : y >= y0 } holds
P is convex

proof end;

registration

let p be Point of (TOP-REAL 2);
cluster north_halfline p -> non empty convex ;
coherence

proof end;

cluster east_halfline p -> non empty convex ;
coherence

proof end;

cluster south_halfline p -> non empty convex ;
coherence

proof end;

cluster west_halfline p -> non empty convex ;
coherence

proof end;

end;

theorem :: JORDAN1A:37

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))

proof end;

theorem :: JORDAN1A:38

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)

proof end;

theorem Th39: :: JORDAN1A:39

for j1, j2, i1, i2 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

proof end;

theorem Th40: :: JORDAN1A:40

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

proof end;

theorem Th41: :: JORDAN1A:41

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)

proof end;

theorem Th42: :: JORDAN1A:42

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)

proof end;

theorem Th43: :: JORDAN1A:43

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)

proof end;

theorem Th44: :: JORDAN1A:44

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)

proof end;

theorem Th45: :: JORDAN1A:45

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

proof end;

theorem Th46: :: JORDAN1A:46

for i, j being Nat
for G being Go-board st i <= len G & j <= width G holds
cell G,i,j is connected

proof end;

theorem Th47: :: JORDAN1A:47

for i being Nat
for G being Go-board st i <= len G holds
not cell G,i,0 is Bounded

proof end;

theorem Th48: :: JORDAN1A:48

for i being Nat
for G being Go-board st i <= len G holds
not cell G,i,(width G) is Bounded

proof end;

theorem :: JORDAN1A:49

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

proof end;

theorem :: JORDAN1A:50

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)

proof end;

theorem :: JORDAN1A:51

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)

proof end;

theorem Th52: :: JORDAN1A:52

for m, n, i 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) )

proof end;

theorem Th53: :: JORDAN1A:53

for m, n, i 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) )

proof end;

theorem Th54: :: JORDAN1A:54

for m, n, i, j 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

proof end;

theorem Th55: :: JORDAN1A:55

for m, n, i 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) )

proof end;

theorem Th56: :: JORDAN1A:56

for m, n, i 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) )

proof end;

Lm9: now

let D be non empty Subset of (TOP-REAL 2); :: thesis:
let n be Nat; :: thesis:
set G = Gauge D,n;
0 + 1 <= ((len (Gauge D,n)) div 2) + 1 by XREAL_1:8;
hence 1 <= Center (Gauge D,n) ; :: thesis:
4 <= len (Gauge D,n) by JORDAN8:13;
then 0 < len (Gauge D,n) ;
then (len (Gauge D,n)) div 2 < len (Gauge D,n) by SCMFSA9A:4;
then (len (Gauge D,n)) div 2 < len (Gauge D,n) by NEWTON:101;
then ((len (Gauge D,n)) div 2) + 1 <= len (Gauge D,n) by NAT_1:38;
hence Center (Gauge D,n) <= len (Gauge D,n) ; :: thesis:

end;

Lm10: now

let D be non empty Subset of (TOP-REAL 2); :: thesis:
let n, j be Nat;
set G = Gauge D,n;
assume A1: ( 1 <= j & j <= len (Gauge D,n) ) ; :: thesis:
A2: len (Gauge D,n) = width (Gauge D,n) by JORDAN8:def 1;
0 + 1 <= ((len (Gauge D,n)) div 2) + 1 by XREAL_1:8;
then A3: 0 + 1 <= Center (Gauge D,n) ;
Center (Gauge D,n) <= len (Gauge D,n) by Lm9;
hence [(Center (Gauge D,n)),j] in Indices (Gauge D,n) by A1, A2, A3, GOBOARD7:10; :: thesis:

end;

Lm11: now

let D be non empty Subset of (TOP-REAL 2); :: thesis:
let n, j be Nat;
set G = Gauge D,n;
assume A1: ( 1 <= j & j <= len (Gauge D,n) ) ; :: thesis:
A2: len (Gauge D,n) = width (Gauge D,n) by JORDAN8:def 1;
0 + 1 <= ((len (Gauge D,n)) div 2) + 1 by XREAL_1:8;
then A3: 0 + 1 <= Center (Gauge D,n) ;
Center (Gauge D,n) <= len (Gauge D,n) by Lm9;
hence [j,(Center (Gauge D,n))] in Indices (Gauge D,n) by A1, A2, A3, GOBOARD7:10; :: thesis:

end;

Lm12: for n being Nat
for D being non empty Subset of (TOP-REAL 2)
for w being real number st n > 0 holds
(w / (2 |^ n)) * ((Center (Gauge D,n)) - 2) = w / 2

proof end;

Lm13: now

let m, n be Nat;
let c, d be real number ; :: thesis:
assume A1: 0 <= c ; :: thesis:
A2: 0 < 2 |^ m by HEINE:5;
assume m <= n ; :: thesis:
then 2 |^ m <= 2 |^ n by PCOMPS_2:4;
hence c / (2 |^ n) <= c / (2 |^ m) by A1, A2, XREAL_1:120; :: thesis:

end;

Lm14: now

let m, n be Nat;
let c, d be real number ; :: thesis:
assume ( 0 <= c & m <= n ) ; :: thesis:
then c / (2 |^ n) <= c / (2 |^ m) by Lm13;
hence d + (c / (2 |^ n)) <= d + (c / (2 |^ m)) by XREAL_1:8; :: thesis:

end;

Lm15: now

let m, n be Nat;
let c, d be real number ; :: thesis:
assume ( 0 <= c & m <= n ) ; :: thesis:
then c / (2 |^ n) <= c / (2 |^ m) by Lm13;
hence d - (c / (2 |^ m)) <= d - (c / (2 |^ n)) by REAL_1:92; :: thesis:

end;

theorem Th57: :: JORDAN1A:57

for i, n, j, m 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

proof end;

theorem :: JORDAN1A:58

for i, n, j, m 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

proof end;

Lm16: now

let D be non empty Subset of (TOP-REAL 2); :: thesis:
let n be Nat; :: thesis:
let e, w be real number ; :: thesis:
A1: 2 |^ n <> 0 by HEINE:5;
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:88
.= e + ((e - w) / (2 |^ n)) ; :: thesis:

end;

Lm17: now

let D be non empty Subset of (TOP-REAL 2); :: thesis:
let n, i be Nat;
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:
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:56 ;
:: thesis:

end;

Lm18: now

let D be non empty Subset of (TOP-REAL 2); :: thesis:
let n, i be Nat;
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:
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:56 ;
:: thesis:

end;

Lm19: now

let D be non empty Subset of (TOP-REAL 2); :: thesis:
let n, i be Nat;
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:
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:56
.= (N-bound D) + (((N-bound D) - (S-bound D)) / (2 |^ n)) by Lm16 ;
:: thesis:

end;

Lm20: now

let D be non empty Subset of (TOP-REAL 2); :: thesis:
let n, i be Nat;
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:
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:56
.= (E-bound D) + (((E-bound D) - (W-bound D)) / (2 |^ n)) by Lm16 ;
:: thesis:

end;

theorem :: JORDAN1A:59

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

proof end;

theorem :: JORDAN1A:60

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

proof end;

theorem Th61: :: JORDAN1A:61

for i, n, j, m 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

proof end;

theorem :: JORDAN1A:62

for i, n, j, m 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

proof end;

theorem :: JORDAN1A:63

for i, n, j, m 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

proof end;

theorem :: JORDAN1A:64

for i, n, j, m 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

proof end;

theorem :: JORDAN1A:65

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)))

proof end;

theorem :: JORDAN1A:66

for m, n, j 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)

proof end;

theorem :: JORDAN1A:67

for m, n, j 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)))

proof end;

theorem Th68: :: JORDAN1A:68

for m, n, i, j 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

proof end;

theorem :: JORDAN1A:69

for m, n, i, j 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

proof end;

theorem :: JORDAN1A:70

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

proof end;

theorem :: JORDAN1A:71

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

proof end;

theorem Th72: :: JORDAN1A:72

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)

proof end;

theorem Th73: :: JORDAN1A:73

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)

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 being Point of (TOP-REAL 2) st p in C holds
south_halfline p meets L~ (Cage C,n)

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 being Point of (TOP-REAL 2) st p in C holds
west_halfline p meets L~ (Cage C,n)

proof end;

Lm21: 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;

Lm22: 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;

Lm23: 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 Th76: :: JORDAN1A:76

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;

theorem Th77: :: JORDAN1A:77

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;

theorem Th78: :: JORDAN1A:78

proof end;

theorem Th79: :: JORDAN1A:79

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))

proof end;

theorem Th80: :: JORDAN1A:80

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))

proof end;

theorem Th81: :: JORDAN1A:81

proof end;

theorem Th82: :: JORDAN1A:82

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))

proof end;

theorem Th83: :: JORDAN1A:83

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))

proof end;

theorem Th84: :: JORDAN1A:84

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))

proof end;

theorem Th85: :: JORDAN1A:85

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))

proof end;

theorem :: JORDAN1A:86

for n, m 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)))

proof end;

theorem :: JORDAN1A:87

for n, m 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)))

proof end;

theorem :: JORDAN1A:88

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))

proof end;

theorem :: JORDAN1A:89

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))

proof end;

theorem :: JORDAN1A:90

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))

proof end;

theorem :: JORDAN1A:91

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

proof end;

theorem :: JORDAN1A:92

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

proof end;

theorem :: JORDAN1A:93

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

proof end;

theorem :: JORDAN1A:94

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

proof end;

Lm24: for p being Point of (TOP-REAL 2)
for C being Subset of (TOP-REAL 2) st p in N-most C holds
p in C

proof end;

Lm25: for p being Point of (TOP-REAL 2)
for C being Subset of (TOP-REAL 2) st p in E-most C holds
p in C

proof end;

Lm26: for p being Point of (TOP-REAL 2)
for C being Subset of (TOP-REAL 2) st p in S-most C holds
p in C

proof end;

Lm27: for p being Point of (TOP-REAL 2)
for C being Subset of (TOP-REAL 2) st p in W-most C holds
p in C

proof end;

theorem Th95: :: JORDAN1A:95

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th96: :: JORDAN1A:96

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th97: :: JORDAN1A:97

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th98: :: JORDAN1A:98

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th99: :: JORDAN1A:99

for i, n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th100: :: JORDAN1A:100

for i, n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th101: :: JORDAN1A:101

for i, n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th102: :: JORDAN1A:102

for i, n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th103: :: JORDAN1A:103

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th104: :: JORDAN1A:104

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th105: :: JORDAN1A:105

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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 Th106: :: JORDAN1A:106

for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for x, p 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:107

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}

proof end;

theorem :: JORDAN1A:108

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}

proof end;

theorem :: JORDAN1A:109

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}

proof end;

theorem :: JORDAN1A:110

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}

proof end;