:: JORDAN1A semantic presentation

3 = (2 * 1) + 1
;

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

1 = (2 * 0) + 1
;

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

Lemma3: for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₁ <= b₃ & 0 <= b₄ & b₄ <= 1 holds
b₁ <= ((1 - b₄) * b₂) + (b₄ * b₃)
by XREAL_1:175;

Lemma4: for b₁, b₂, b₃, b₄ being real number st b₂ <= b₁ & b₃ <= b₁ & 0 <= b₄ & b₄ <= 1 holds
((1 - b₄) * b₂) + (b₄ * b₃) <= b₁
by XREAL_1:176;

theorem Th1: :: JORDAN1A:1

canceled;

theorem Th2: :: JORDAN1A:2

canceled;

theorem Th3: :: JORDAN1A:3

canceled;

theorem Th4: :: JORDAN1A:4

for b₁, b₂ being natural number st b₂ > 0 & b₁ mod b₂ = 0 holds
b₁ div b₂ = b₁ / b₂

proof end;

theorem Th5: :: JORDAN1A:5

for b₁, b₂ being natural number st b₂ > 0 holds
(b₁ |^ b₂) div b₁ = (b₁ |^ b₂) / b₁

proof end;

theorem Th6: :: JORDAN1A:6

for b₁ being real number
for b₂ being natural number st 0 < b₂ & 1 < b₁ holds
1 < b₁ |^ b₂

proof end;

theorem Th7: :: JORDAN1A:7

for b₁ being real number
for b₂, b₃ being natural number st b₁ > 1 & b₂ > b₃ holds
b₁ |^ b₂ > b₁ |^ b₃

proof end;

theorem Th8: :: JORDAN1A:8

for b₁ being non empty TopSpace
for b₂, b₃, b₄ being Subset of b₁ st b₂ is connected & b₄ is_a_component_of b₃ & b₂ meets b₄ & b₂ c= b₃ holds
b₂ c= b₄

proof end;

definition

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

end;

:: deftheorem Def1 defines Center JORDAN1A:def 1 :

theorem Th9: :: JORDAN1A:9

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

proof end;

theorem Th10: :: JORDAN1A:10

for b₁ being FinSequence st len b₁ is even holds
len b₁ = (2 * (Center b₁)) - 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 b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in N-most b₁ holds
b₂ `2 = N-bound b₁

proof end;

theorem Th12: :: JORDAN1A:12

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in E-most b₁ holds
b₂ `1 = E-bound b₁

proof end;

theorem Th13: :: JORDAN1A:13

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in S-most b₁ holds
b₂ `2 = S-bound b₁

proof end;

theorem Th14: :: JORDAN1A:14

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in W-most b₁ holds
b₂ `1 = W-bound b₁

proof end;

theorem Th15: :: JORDAN1A:15

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

proof end;

theorem Th16: :: JORDAN1A:16

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

proof end;

theorem Th17: :: JORDAN1A:17

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

proof end;

theorem Th18: :: JORDAN1A:18

for b₁, b₂ being real number holds |[b₁,b₂]| in Vertical_Line b₁

proof end;

theorem Th19: :: JORDAN1A:19

for b₁ being real number
for b₂ being Subset of (TOP-REAL 2) st b₂ c= Vertical_Line b₁ holds
b₂ is vertical

proof end;

theorem Th20: :: JORDAN1A:20

for b₁, b₂ being real number holds
( proj2 . |[b₁,b₂]| = b₂ & proj1 . |[b₁,b₂]| = b₁ )

proof end;

theorem Th21: :: JORDAN1A:21

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being real number st b₁ `1 = b₂ `1 & b₃ in [.(proj2 . b₁),(proj2 . b₂).] holds
|[(b₁ `1 ),b₃]| in LSeg b₁,b₂

proof end;

theorem Th22: :: JORDAN1A:22

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being real number st b₁ `2 = b₂ `2 & b₃ in [.(proj1 . b₁),(proj1 . b₂).] holds
|[b₃,(b₁ `2 )]| in LSeg b₁,b₂

proof end;

theorem Th23: :: JORDAN1A:23

for b₁, b₂ being Point of (TOP-REAL 2)
for b₃ being real number st b₁ in Vertical_Line b₃ & b₂ in Vertical_Line b₃ holds
LSeg b₁,b₂ c= Vertical_Line b₃

proof end;

registration

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

proof end;

cluster Upper_Arc a₁ -> compact ;
coherence

proof end;

end;

theorem Th24: :: JORDAN1A:24

for b₁, b₂ being Subset of (TOP-REAL 2) st b₁ meets b₂ holds
proj2 .: b₁ meets proj2 .: b₂

proof end;

theorem Th25: :: JORDAN1A:25

for b₁ being real number
for b₂, b₃ being Subset of (TOP-REAL 2) st b₂ misses b₃ & b₂ c= Vertical_Line b₁ & b₃ c= Vertical_Line b₁ holds
proj2 .: b₂ misses proj2 .: b₃

proof end;

theorem Th26: :: JORDAN1A:26

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

proof end;

theorem Th27: :: JORDAN1A:27

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

proof end;

theorem Th28: :: JORDAN1A:28

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

proof end;

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

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

proof end;

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

for b₁, b₂ being Subset of (TOP-REAL F₁()) st ( for b₃ being Point of (TOP-REAL F₁()) holds
( b₃ in b₁ iff P₁[b₃] ) ) & ( for b₃ being Point of (TOP-REAL F₁()) holds
( b₃ in b₂ iff P₁[b₃] ) ) holds
b₁ = b₂

proof end;

definition

let c₁ be Point of (TOP-REAL 2);
func north_halfline c₁ -> Subset of (TOP-REAL 2) means :Def2: :: JORDAN1A:def 2
for b₁ being Point of (TOP-REAL 2) holds
( b₁ in a₂ iff ( b₁ `1 = a₁ `1 & b₁ `2 >= a₁ `2 ) );
existence

proof end;

uniqueness

proof end;

func east_halfline c₁ -> Subset of (TOP-REAL 2) means :Def3: :: JORDAN1A:def 3
for b₁ being Point of (TOP-REAL 2) holds
( b₁ in a₂ iff ( b₁ `1 >= a₁ `1 & b₁ `2 = a₁ `2 ) );
existence

proof end;

uniqueness

proof end;

func south_halfline c₁ -> Subset of (TOP-REAL 2) means :Def4: :: JORDAN1A:def 4
for b₁ being Point of (TOP-REAL 2) holds
( b₁ in a₂ iff ( b₁ `1 = a₁ `1 & b₁ `2 <= a₁ `2 ) );
existence

proof end;

uniqueness

proof end;

func west_halfline c₁ -> Subset of (TOP-REAL 2) means :Def5: :: JORDAN1A:def 5
for b₁ being Point of (TOP-REAL 2) holds
( b₁ in a₂ iff ( b₁ `1 <= a₁ `1 & b₁ `2 = a₁ `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 b₁ being Point of (TOP-REAL 2) holds north_halfline b₁ = { b₂ where B is Point of (TOP-REAL 2) : ( b₂ `1 = b₁ `1 & b₂ `2 >= b₁ `2 ) }

proof end;

theorem Th30: :: JORDAN1A:30

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

proof end;

theorem Th31: :: JORDAN1A:31

for b₁ being Point of (TOP-REAL 2) holds east_halfline b₁ = { b₂ where B is Point of (TOP-REAL 2) : ( b₂ `1 >= b₁ `1 & b₂ `2 = b₁ `2 ) }

proof end;

theorem Th32: :: JORDAN1A:32

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

proof end;

theorem Th33: :: JORDAN1A:33

for b₁ being Point of (TOP-REAL 2) holds south_halfline b₁ = { b₂ where B is Point of (TOP-REAL 2) : ( b₂ `1 = b₁ `1 & b₂ `2 <= b₁ `2 ) }

proof end;

theorem Th34: :: JORDAN1A:34

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

proof end;

theorem Th35: :: JORDAN1A:35

for b₁ being Point of (TOP-REAL 2) holds west_halfline b₁ = { b₂ where B is Point of (TOP-REAL 2) : ( b₂ `1 <= b₁ `1 & b₂ `2 = b₁ `2 ) }

proof end;

theorem Th36: :: JORDAN1A:36

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

proof end;

Lemma29: for b₁, b₂ being real number
for b₃ being Subset of (TOP-REAL 2) st b₃ = { |[b₄,b₂]| where B is Real : b₄ <= b₁ } holds
b₃ is convex

proof end;

Lemma30: for b₁, b₂ being real number
for b₃ being Subset of (TOP-REAL 2) st b₃ = { |[b₁,b₄]| where B is Real : b₄ <= b₂ } holds
b₃ is convex

proof end;

Lemma31: for b₁, b₂ being real number
for b₃ being Subset of (TOP-REAL 2) st b₃ = { |[b₄,b₂]| where B is Real : b₄ >= b₁ } holds
b₃ is convex

proof end;

Lemma32: for b₁, b₂ being real number
for b₃ being Subset of (TOP-REAL 2) st b₃ = { |[b₁,b₄]| where B is Real : b₄ >= b₂ } holds
b₃ is convex

proof end;

registration

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

proof end;

cluster east_halfline a₁ -> non empty convex ;
coherence

proof end;

cluster south_halfline a₁ -> non empty convex ;
coherence

proof end;

cluster west_halfline a₁ -> non empty convex ;
coherence

proof end;

end;

theorem Th37: :: JORDAN1A:37

for b₁, b₂ being Nat
for b₃ being Go-board st 1 <= b₁ & b₁ <= len b₃ & 1 <= b₂ & b₂ <= width b₃ holds
b₃ * b₁,b₂ in LSeg (b₃ * b₁,1),(b₃ * b₁,(width b₃))

proof end;

theorem Th38: :: JORDAN1A:38

for b₁, b₂ being Nat
for b₃ being Go-board st 1 <= b₁ & b₁ <= len b₃ & 1 <= b₂ & b₂ <= width b₃ holds
b₃ * b₁,b₂ in LSeg (b₃ * 1,b₂),(b₃ * (len b₃),b₂)

proof end;

theorem Th39: :: JORDAN1A:39

for b₁, b₂, b₃, b₄ being Nat
for b₅ being Go-board st 1 <= b₁ & b₁ <= width b₅ & 1 <= b₂ & b₂ <= width b₅ & 1 <= b₃ & b₃ <= b₄ & b₄ <= len b₅ holds
(b₅ * b₃,b₁) `1 <= (b₅ * b₄,b₂) `1

proof end;

theorem Th40: :: JORDAN1A:40

for b₁, b₂, b₃, b₄ being Nat
for b₅ being Go-board st 1 <= b₁ & b₁ <= len b₅ & 1 <= b₂ & b₂ <= len b₅ & 1 <= b₃ & b₃ <= b₄ & b₄ <= width b₅ holds
(b₅ * b₁,b₃) `2 <= (b₅ * b₂,b₄) `2

proof end;

theorem Th41: :: JORDAN1A:41

for b₁ being Nat
for b₂ being Go-board
for b₃ being non constant standard special_circular_sequence st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ <= len b₂ holds
(b₂ * b₁,(width b₂)) `2 >= N-bound (L~ b₃)

proof end;

theorem Th42: :: JORDAN1A:42

for b₁ being Nat
for b₂ being Go-board
for b₃ being non constant standard special_circular_sequence st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ <= width b₂ holds
(b₂ * 1,b₁) `1 <= W-bound (L~ b₃)

proof end;

theorem Th43: :: JORDAN1A:43

for b₁ being Nat
for b₂ being Go-board
for b₃ being non constant standard special_circular_sequence st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ <= len b₂ holds
(b₂ * b₁,1) `2 <= S-bound (L~ b₃)

proof end;

theorem Th44: :: JORDAN1A:44

for b₁ being Nat
for b₂ being Go-board
for b₃ being non constant standard special_circular_sequence st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ <= width b₂ holds
(b₂ * (len b₂),b₁) `1 >= E-bound (L~ b₃)

proof end;

theorem Th45: :: JORDAN1A:45

for b₁, b₂ being Nat
for b₃ being Go-board st b₁ <= len b₃ & b₂ <= width b₃ holds
not cell b₃,b₁,b₂ is empty

proof end;

theorem Th46: :: JORDAN1A:46

for b₁, b₂ being Nat
for b₃ being Go-board st b₁ <= len b₃ & b₂ <= width b₃ holds
cell b₃,b₁,b₂ is connected

proof end;

theorem Th47: :: JORDAN1A:47

for b₁ being Nat
for b₂ being Go-board st b₁ <= len b₂ holds
not cell b₂,b₁,0 is Bounded

proof end;

theorem Th48: :: JORDAN1A:48

for b₁ being Nat
for b₂ being Go-board st b₁ <= len b₂ holds
not cell b₂,b₁,(width b₂) is Bounded

proof end;

theorem Th49: :: JORDAN1A:49

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

proof end;

theorem Th50: :: JORDAN1A:50

for b₁, b₂ being Nat
for b₃ being non empty Subset of (TOP-REAL 2) st b₁ < b₂ holds
len (Gauge b₃,b₁) < len (Gauge b₃,b₂)

proof end;

theorem Th51: :: JORDAN1A:51

for b₁, b₂ being Nat
for b₃ being non empty Subset of (TOP-REAL 2) st b₁ <= b₂ holds
len (Gauge b₃,b₁) <= len (Gauge b₃,b₂)

proof end;

theorem Th52: :: JORDAN1A:52

for b₁, b₂, b₃ being Nat
for b₄ being non empty Subset of (TOP-REAL 2) st b₁ <= b₂ & 1 < b₃ & b₃ < len (Gauge b₄,b₁) holds
( 1 < ((2 |^ (b₂ -' b₁)) * (b₃ - 2)) + 2 & ((2 |^ (b₂ -' b₁)) * (b₃ - 2)) + 2 < len (Gauge b₄,b₂) )

proof end;

theorem Th53: :: JORDAN1A:53

for b₁, b₂, b₃ being Nat
for b₄ being non empty Subset of (TOP-REAL 2) st b₁ <= b₂ & 1 < b₃ & b₃ < width (Gauge b₄,b₁) holds
( 1 < ((2 |^ (b₂ -' b₁)) * (b₃ - 2)) + 2 & ((2 |^ (b₂ -' b₁)) * (b₃ - 2)) + 2 < width (Gauge b₄,b₂) )

proof end;

theorem Th54: :: JORDAN1A:54

for b₁, b₂, b₃, b₄ being Nat
for b₅ being non empty Subset of (TOP-REAL 2) st b₁ <= b₂ & 1 < b₃ & b₃ < len (Gauge b₅,b₁) & 1 < b₄ & b₄ < width (Gauge b₅,b₁) holds
for b₆, b₇ being Nat st b₆ = ((2 |^ (b₂ -' b₁)) * (b₃ - 2)) + 2 & b₇ = ((2 |^ (b₂ -' b₁)) * (b₄ - 2)) + 2 holds
(Gauge b₅,b₁) * b₃,b₄ = (Gauge b₅,b₂) * b₆,b₇

proof end;

theorem Th55: :: JORDAN1A:55

for b₁, b₂, b₃ being Nat
for b₄ being non empty Subset of (TOP-REAL 2) st b₁ <= b₂ & 1 < b₃ & b₃ + 1 < len (Gauge b₄,b₁) holds
( 1 < ((2 |^ (b₂ -' b₁)) * (b₃ - 1)) + 2 & ((2 |^ (b₂ -' b₁)) * (b₃ - 1)) + 2 <= len (Gauge b₄,b₂) )

proof end;

theorem Th56: :: JORDAN1A:56

for b₁, b₂, b₃ being Nat
for b₄ being non empty Subset of (TOP-REAL 2) st b₁ <= b₂ & 1 < b₃ & b₃ + 1 < width (Gauge b₄,b₁) holds
( 1 < ((2 |^ (b₂ -' b₁)) * (b₃ - 1)) + 2 & ((2 |^ (b₂ -' b₁)) * (b₃ - 1)) + 2 <= width (Gauge b₄,b₂) )

proof end;

E48: now

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

end;

E49: now

let c₁ be non empty Subset of (TOP-REAL 2);
let c₂, c₃ be Nat;
set c₄ = Gauge c₁,c₂;
assume E50: ( 1 <= c₃ & c₃ <= len (Gauge c₁,c₂) ) ;
E51: len (Gauge c₁,c₂) = width (Gauge c₁,c₂) by JORDAN8:def 1;
0 + 1 <= ((len (Gauge c₁,c₂)) div 2) + 1 by XREAL_1:8;
then E52: 0 + 1 <= Center (Gauge c₁,c₂) ;
Center (Gauge c₁,c₂) <= len (Gauge c₁,c₂) by Lemma48;
hence [(Center (Gauge c₁,c₂)),c₃] in Indices (Gauge c₁,c₂) by E50, E51, E52, GOBOARD7:10;

end;

E50: now

let c₁ be non empty Subset of (TOP-REAL 2);
let c₂, c₃ be Nat;
set c₄ = Gauge c₁,c₂;
assume E51: ( 1 <= c₃ & c₃ <= len (Gauge c₁,c₂) ) ;
E52: len (Gauge c₁,c₂) = width (Gauge c₁,c₂) by JORDAN8:def 1;
0 + 1 <= ((len (Gauge c₁,c₂)) div 2) + 1 by XREAL_1:8;
then E53: 0 + 1 <= Center (Gauge c₁,c₂) ;
Center (Gauge c₁,c₂) <= len (Gauge c₁,c₂) by Lemma48;
hence [c₃,(Center (Gauge c₁,c₂))] in Indices (Gauge c₁,c₂) by E51, E52, E53, GOBOARD7:10;

end;

Lemma51: for b₁ being Nat
for b₂ being non empty Subset of (TOP-REAL 2)
for b₃ being real number st b₁ > 0 holds
(b₃ / (2 |^ b₁)) * ((Center (Gauge b₂,b₁)) - 2) = b₃ / 2

proof end;

E52: now

end;

E53: now

let c₁, c₂ be Nat;
let c₃, c₄ be real number ;
assume ( 0 <= c₃ & c₁ <= c₂ ) ;
then c₃ / (2 |^ c₂) <= c₃ / (2 |^ c₁) by Lemma52;
hence c₄ + (c₃ / (2 |^ c₂)) <= c₄ + (c₃ / (2 |^ c₁)) by XREAL_1:8;

end;

E54: now

let c₁, c₂ be Nat;
let c₃, c₄ be real number ;
assume ( 0 <= c₃ & c₁ <= c₂ ) ;
then c₃ / (2 |^ c₂) <= c₃ / (2 |^ c₁) by Lemma52;
hence c₄ - (c₃ / (2 |^ c₁)) <= c₄ - (c₃ / (2 |^ c₂)) by REAL_1:92;

end;

theorem Th57: :: JORDAN1A:57

for b₁, b₂, b₃, b₄ being Nat
for b₅ being non empty Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₅,b₂) & 1 <= b₃ & b₃ <= len (Gauge b₅,b₄) & ( ( b₂ > 0 & b₄ > 0 ) or ( b₂ = 0 & b₄ = 0 ) ) holds
((Gauge b₅,b₂) * (Center (Gauge b₅,b₂)),b₁) `1 = ((Gauge b₅,b₄) * (Center (Gauge b₅,b₄)),b₃) `1

proof end;

theorem Th58: :: JORDAN1A:58

for b₁, b₂, b₃, b₄ being Nat
for b₅ being non empty Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₅,b₂) & 1 <= b₃ & b₃ <= len (Gauge b₅,b₄) & ( ( b₂ > 0 & b₄ > 0 ) or ( b₂ = 0 & b₄ = 0 ) ) holds
((Gauge b₅,b₂) * b₁,(Center (Gauge b₅,b₂))) `2 = ((Gauge b₅,b₄) * b₃,(Center (Gauge b₅,b₄))) `2

proof end;

E56: now

let c₁ be non empty Subset of (TOP-REAL 2);
let c₂ be Nat;
let c₃, c₄ be real number ;
E57: 2 |^ c₂ <> 0 by HEINE:5;
thus c₄ + (((c₃ - c₄) / (2 |^ c₂)) * ((len (Gauge c₁,c₂)) - 2)) = c₄ + (((c₃ - c₄) / (2 |^ c₂)) * (((2 |^ c₂) + 3) - 2)) by JORDAN8:def 1
.= (c₄ + (((c₃ - c₄) / (2 |^ c₂)) * (2 |^ c₂))) + ((c₃ - c₄) / (2 |^ c₂))
.= (c₄ + (c₃ - c₄)) + ((c₃ - c₄) / (2 |^ c₂)) by E57, XCMPLX_1:88
.= c₃ + ((c₃ - c₄) / (2 |^ c₂)) ;

end;

E57: now

let c₁ be non empty Subset of (TOP-REAL 2);
let c₂, c₃ be Nat;
set c₄ = N-bound c₁;
set c₅ = S-bound c₁;
set c₆ = W-bound c₁;
set c₇ = E-bound c₁;
set c₈ = Gauge c₁,c₂;
assume [c₃,1] in Indices (Gauge c₁,c₂) ;
hence ((Gauge c₁,c₂) * c₃,1) `2 = |[((W-bound c₁) + ((((E-bound c₁) - (W-bound c₁)) / (2 |^ c₂)) * (c₃ - 2))),((S-bound c₁) + ((((N-bound c₁) - (S-bound c₁)) / (2 |^ c₂)) * (1 - 2)))]| `2 by JORDAN8:def 1
.= (S-bound c₁) - (((N-bound c₁) - (S-bound c₁)) / (2 |^ c₂)) by EUCLID:56 ;

end;

E58: now

let c₁ be non empty Subset of (TOP-REAL 2);
let c₂, c₃ be Nat;
set c₄ = N-bound c₁;
set c₅ = S-bound c₁;
set c₆ = W-bound c₁;
set c₇ = E-bound c₁;
set c₈ = Gauge c₁,c₂;
assume [1,c₃] in Indices (Gauge c₁,c₂) ;
hence ((Gauge c₁,c₂) * 1,c₃) `1 = |[((W-bound c₁) + ((((E-bound c₁) - (W-bound c₁)) / (2 |^ c₂)) * (1 - 2))),((S-bound c₁) + ((((N-bound c₁) - (S-bound c₁)) / (2 |^ c₂)) * (c₃ - 2)))]| `1 by JORDAN8:def 1
.= (W-bound c₁) - (((E-bound c₁) - (W-bound c₁)) / (2 |^ c₂)) by EUCLID:56 ;

end;

E59: now

let c₁ be non empty Subset of (TOP-REAL 2);
let c₂, c₃ be Nat;
set c₄ = N-bound c₁;
set c₅ = S-bound c₁;
set c₆ = W-bound c₁;
set c₇ = E-bound c₁;
set c₈ = Gauge c₁,c₂;
assume [c₃,(len (Gauge c₁,c₂))] in Indices (Gauge c₁,c₂) ;
hence ((Gauge c₁,c₂) * c₃,(len (Gauge c₁,c₂))) `2 = |[((W-bound c₁) + ((((E-bound c₁) - (W-bound c₁)) / (2 |^ c₂)) * (c₃ - 2))),((S-bound c₁) + ((((N-bound c₁) - (S-bound c₁)) / (2 |^ c₂)) * ((len (Gauge c₁,c₂)) - 2)))]| `2 by JORDAN8:def 1
.= (S-bound c₁) + ((((N-bound c₁) - (S-bound c₁)) / (2 |^ c₂)) * ((len (Gauge c₁,c₂)) - 2)) by EUCLID:56
.= (N-bound c₁) + (((N-bound c₁) - (S-bound c₁)) / (2 |^ c₂)) by Lemma56 ;

end;

E60: now

let c₁ be non empty Subset of (TOP-REAL 2);
let c₂, c₃ be Nat;
set c₄ = N-bound c₁;
set c₅ = S-bound c₁;
set c₆ = W-bound c₁;
set c₇ = E-bound c₁;
set c₈ = Gauge c₁,c₂;
assume [(len (Gauge c₁,c₂)),c₃] in Indices (Gauge c₁,c₂) ;
hence ((Gauge c₁,c₂) * (len (Gauge c₁,c₂)),c₃) `1 = |[((W-bound c₁) + ((((E-bound c₁) - (W-bound c₁)) / (2 |^ c₂)) * ((len (Gauge c₁,c₂)) - 2))),((S-bound c₁) + ((((N-bound c₁) - (S-bound c₁)) / (2 |^ c₂)) * (c₃ - 2)))]| `1 by JORDAN8:def 1
.= (W-bound c₁) + ((((E-bound c₁) - (W-bound c₁)) / (2 |^ c₂)) * ((len (Gauge c₁,c₂)) - 2)) by EUCLID:56
.= (E-bound c₁) + (((E-bound c₁) - (W-bound c₁)) / (2 |^ c₂)) by Lemma56 ;

end;

theorem Th59: :: JORDAN1A:59

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₂,1) holds
((Gauge b₂,1) * (Center (Gauge b₂,1)),b₁) `1 = ((W-bound b₂) + (E-bound b₂)) / 2

proof end;

theorem Th60: :: JORDAN1A:60

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₂,1) holds
((Gauge b₂,1) * b₁,(Center (Gauge b₂,1))) `2 = ((S-bound b₂) + (N-bound b₂)) / 2

proof end;

theorem Th61: :: JORDAN1A:61

for b₁, b₂, b₃, b₄ being Nat
for b₅ being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₅,b₂) & 1 <= b₃ & b₃ <= len (Gauge b₅,b₄) & b₄ <= b₂ holds
((Gauge b₅,b₂) * b₁,(len (Gauge b₅,b₂))) `2 <= ((Gauge b₅,b₄) * b₃,(len (Gauge b₅,b₄))) `2

proof end;

theorem Th62: :: JORDAN1A:62

for b₁, b₂, b₃, b₄ being Nat
for b₅ being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₅,b₂) & 1 <= b₃ & b₃ <= len (Gauge b₅,b₄) & b₄ <= b₂ holds
((Gauge b₅,b₂) * (len (Gauge b₅,b₂)),b₁) `1 <= ((Gauge b₅,b₄) * (len (Gauge b₅,b₄)),b₃) `1

proof end;

theorem Th63: :: JORDAN1A:63

proof end;

theorem Th64: :: JORDAN1A:64

proof end;

theorem Th65: :: JORDAN1A:65

for b₁, b₂ being Nat
for b₃ being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= b₂ holds
LSeg ((Gauge b₃,b₂) * (Center (Gauge b₃,b₂)),1),((Gauge b₃,b₂) * (Center (Gauge b₃,b₂)),(len (Gauge b₃,b₂))) c= LSeg ((Gauge b₃,b₁) * (Center (Gauge b₃,b₁)),1),((Gauge b₃,b₁) * (Center (Gauge b₃,b₁)),(len (Gauge b₃,b₁)))

proof end;

theorem Th66: :: JORDAN1A:66

for b₁, b₂, b₃ being Nat
for b₄ being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= b₂ & 1 <= b₃ & b₃ <= width (Gauge b₄,b₂) holds
LSeg ((Gauge b₄,b₂) * (Center (Gauge b₄,b₂)),1),((Gauge b₄,b₂) * (Center (Gauge b₄,b₂)),b₃) c= LSeg ((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),1),((Gauge b₄,b₂) * (Center (Gauge b₄,b₂)),b₃)

proof end;

theorem Th67: :: JORDAN1A:67

for b₁, b₂, b₃ being Nat
for b₄ being compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= b₂ & 1 <= b₃ & b₃ <= width (Gauge b₄,b₂) holds
LSeg ((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),1),((Gauge b₄,b₂) * (Center (Gauge b₄,b₂)),b₃) c= LSeg ((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),1),((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),(len (Gauge b₄,b₁)))

proof end;

theorem Th68: :: JORDAN1A:68

for b₁, b₂, b₃, b₄ being Nat
for b₅ being compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ <= b₂ & 1 < b₃ & b₃ + 1 < len (Gauge b₅,b₁) & 1 < b₄ & b₄ + 1 < width (Gauge b₅,b₁) holds
for b₆, b₇ being Nat st ((2 |^ (b₂ -' b₁)) * (b₃ - 2)) + 2 <= b₆ & b₆ < ((2 |^ (b₂ -' b₁)) * (b₃ - 1)) + 2 & ((2 |^ (b₂ -' b₁)) * (b₄ - 2)) + 2 <= b₇ & b₇ < ((2 |^ (b₂ -' b₁)) * (b₄ - 1)) + 2 holds
cell (Gauge b₅,b₂),b₆,b₇ c= cell (Gauge b₅,b₁),b₃,b₄

proof end;

theorem Th69: :: JORDAN1A:69

for b₁, b₂, b₃, b₄ being Nat
for b₅ being compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ <= b₂ & 3 <= b₃ & b₃ < len (Gauge b₅,b₁) & 1 < b₄ & b₄ + 1 < width (Gauge b₅,b₁) holds
for b₆, b₇ being Nat st b₆ = ((2 |^ (b₂ -' b₁)) * (b₃ - 2)) + 2 & b₇ = ((2 |^ (b₂ -' b₁)) * (b₄ - 2)) + 2 holds
cell (Gauge b₅,b₂),(b₆ -' 1),b₇ c= cell (Gauge b₅,b₁),(b₃ -' 1),b₄

proof end;

theorem Th70: :: JORDAN1A:70

for b₁, b₂ being Nat
for b₃ being compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ <= len (Gauge b₃,b₂) holds
cell (Gauge b₃,b₂),b₁,0 c= UBD b₃

proof end;

theorem Th71: :: JORDAN1A:71

for b₁, b₂ being Nat
for b₃, b₄ being compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ <= len (Gauge b₃,b₂) holds
cell (Gauge b₃,b₂),b₁,(width (Gauge b₃,b₂)) c= UBD b₃

proof end;

theorem Th72: :: JORDAN1A:72

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in b₂ holds
north_halfline b₃ meets L~ (Cage b₂,b₁)

proof end;

theorem Th73: :: JORDAN1A:73

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in b₂ holds
east_halfline b₃ meets L~ (Cage b₂,b₁)

proof end;

theorem Th74: :: JORDAN1A:74

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in b₂ holds
south_halfline b₃ meets L~ (Cage b₂,b₁)

proof end;

theorem Th75: :: JORDAN1A:75

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in b₂ holds
west_halfline b₃ meets L~ (Cage b₂,b₁)

proof end;

Lemma67: for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b₃, b₄ being Nat st
( 1 <= b₃ & b₃ <= len (Cage b₂,b₁) & 1 <= b₄ & b₄ <= width (Gauge b₂,b₁) & (Cage b₂,b₁) /. b₃ = (Gauge b₂,b₁) * 1,b₄ )

proof end;

Lemma68: for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b₃, b₄ being Nat st
( 1 <= b₃ & b₃ <= len (Cage b₂,b₁) & 1 <= b₄ & b₄ <= len (Gauge b₂,b₁) & (Cage b₂,b₁) /. b₃ = (Gauge b₂,b₁) * b₄,1 )

proof end;

Lemma69: for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b₃, b₄ being Nat st
( 1 <= b₃ & b₃ <= len (Cage b₂,b₁) & 1 <= b₄ & b₄ <= width (Gauge b₂,b₁) & (Cage b₂,b₁) /. b₃ = (Gauge b₂,b₁) * (len (Gauge b₂,b₁)),b₄ )

proof end;

theorem Th76: :: JORDAN1A:76

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b₃, b₄ being Nat st
( 1 <= b₃ & b₃ < len (Cage b₂,b₁) & 1 <= b₄ & b₄ <= width (Gauge b₂,b₁) & (Cage b₂,b₁) /. b₃ = (Gauge b₂,b₁) * 1,b₄ )

proof end;

theorem Th77: :: JORDAN1A:77

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) ex b₃, b₄ being Nat st
( 1 <= b₃ & b₃ < len (Cage b₂,b₁) & 1 <= b₄ & b₄ <= len (Gauge b₂,b₁) & (Cage b₂,b₁) /. b₃ = (Gauge b₂,b₁) * b₄,1 )

proof end;

theorem Th78: :: JORDAN1A:78

proof end;

theorem Th79: :: JORDAN1A:79

for b₁, b₂, b₃ being Nat
for b₄ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Cage b₄,b₂) & 1 <= b₃ & b₃ <= len (Gauge b₄,b₂) & (Cage b₄,b₂) /. b₁ = (Gauge b₄,b₂) * b₃,(width (Gauge b₄,b₂)) holds
(Cage b₄,b₂) /. b₁ in N-most (L~ (Cage b₄,b₂))

proof end;

theorem Th80: :: JORDAN1A:80

for b₁, b₂, b₃ being Nat
for b₄ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Cage b₄,b₂) & 1 <= b₃ & b₃ <= width (Gauge b₄,b₂) & (Cage b₄,b₂) /. b₁ = (Gauge b₄,b₂) * 1,b₃ holds
(Cage b₄,b₂) /. b₁ in W-most (L~ (Cage b₄,b₂))

proof end;

theorem Th81: :: JORDAN1A:81

for b₁, b₂, b₃ being Nat
for b₄ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Cage b₄,b₂) & 1 <= b₃ & b₃ <= len (Gauge b₄,b₂) & (Cage b₄,b₂) /. b₁ = (Gauge b₄,b₂) * b₃,1 holds
(Cage b₄,b₂) /. b₁ in S-most (L~ (Cage b₄,b₂))

proof end;

theorem Th82: :: JORDAN1A:82

for b₁, b₂, b₃ being Nat
for b₄ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Cage b₄,b₂) & 1 <= b₃ & b₃ <= width (Gauge b₄,b₂) & (Cage b₄,b₂) /. b₁ = (Gauge b₄,b₂) * (len (Gauge b₄,b₂)),b₃ holds
(Cage b₄,b₂) /. b₁ in E-most (L~ (Cage b₄,b₂))

proof end;

theorem Th83: :: JORDAN1A:83

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

proof end;

theorem Th84: :: JORDAN1A:84

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

proof end;

theorem Th85: :: JORDAN1A:85

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

proof end;

theorem Th86: :: JORDAN1A:86

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-bound (L~ (Cage b₃,b₁))) + (S-bound (L~ (Cage b₃,b₁))) = (N-bound (L~ (Cage b₃,b₂))) + (S-bound (L~ (Cage b₃,b₂)))

proof end;

theorem Th87: :: JORDAN1A:87

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-bound (L~ (Cage b₃,b₁))) + (W-bound (L~ (Cage b₃,b₁))) = (E-bound (L~ (Cage b₃,b₂))) + (W-bound (L~ (Cage b₃,b₂)))

proof end;

theorem Th88: :: JORDAN1A:88

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ < b₂ holds
E-bound (L~ (Cage b₃,b₂)) < E-bound (L~ (Cage b₃,b₁))

proof end;

theorem Th89: :: JORDAN1A:89

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ < b₂ holds
W-bound (L~ (Cage b₃,b₁)) < W-bound (L~ (Cage b₃,b₂))

proof end;

theorem Th90: :: JORDAN1A:90

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st b₁ < b₂ holds
S-bound (L~ (Cage b₃,b₁)) < S-bound (L~ (Cage b₃,b₂))

proof end;

theorem Th91: :: JORDAN1A:91

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₃,b₂) holds
N-bound (L~ (Cage b₃,b₂)) = ((Gauge b₃,b₂) * b₁,(len (Gauge b₃,b₂))) `2

proof end;

theorem Th92: :: JORDAN1A:92

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₃,b₂) holds
E-bound (L~ (Cage b₃,b₂)) = ((Gauge b₃,b₂) * (len (Gauge b₃,b₂)),b₁) `1

proof end;

theorem Th93: :: JORDAN1A:93

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₃,b₂) holds
S-bound (L~ (Cage b₃,b₂)) = ((Gauge b₃,b₂) * b₁,1) `2

proof end;

theorem Th94: :: JORDAN1A:94

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2) st 1 <= b₁ & b₁ <= len (Gauge b₃,b₂) holds
W-bound (L~ (Cage b₃,b₂)) = ((Gauge b₃,b₂) * 1,b₁) `1

proof end;

Lemma80: for b₁ being Point of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) st b₁ in N-most b₂ holds
b₁ in b₂

proof end;

Lemma81: for b₁ being Point of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) st b₁ in E-most b₂ holds
b₁ in b₂

proof end;

Lemma82: for b₁ being Point of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) st b₁ in S-most b₂ holds
b₁ in b₂

proof end;

Lemma83: for b₁ being Point of (TOP-REAL 2)
for b₂ being Subset of (TOP-REAL 2) st b₁ in W-most b₂ holds
b₁ in b₂

proof end;

theorem Th95: :: JORDAN1A:95

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in b₂ & b₄ in (north_halfline b₃) /\ (L~ (Cage b₂,b₁)) holds
b₄ `2 > b₃ `2

proof end;

theorem Th96: :: JORDAN1A:96

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in b₂ & b₄ in (east_halfline b₃) /\ (L~ (Cage b₂,b₁)) holds
b₄ `1 > b₃ `1

proof end;

theorem Th97: :: JORDAN1A:97

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in b₂ & b₄ in (south_halfline b₃) /\ (L~ (Cage b₂,b₁)) holds
b₄ `2 < b₃ `2

proof end;

theorem Th98: :: JORDAN1A:98

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in b₂ & b₄ in (west_halfline b₃) /\ (L~ (Cage b₂,b₁)) holds
b₄ `1 < b₃ `1

proof end;

theorem Th99: :: JORDAN1A:99

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ in N-most b₃ & b₅ in north_halfline b₄ & 1 <= b₁ & b₁ < len (Cage b₃,b₂) & b₅ in LSeg (Cage b₃,b₂),b₁ holds
LSeg (Cage b₃,b₂),b₁ is horizontal

proof end;

theorem Th100: :: JORDAN1A:100

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ in E-most b₃ & b₅ in east_halfline b₄ & 1 <= b₁ & b₁ < len (Cage b₃,b₂) & b₅ in LSeg (Cage b₃,b₂),b₁ holds
LSeg (Cage b₃,b₂),b₁ is vertical

proof end;

theorem Th101: :: JORDAN1A:101

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ in S-most b₃ & b₅ in south_halfline b₄ & 1 <= b₁ & b₁ < len (Cage b₃,b₂) & b₅ in LSeg (Cage b₃,b₂),b₁ holds
LSeg (Cage b₃,b₂),b₁ is horizontal

proof end;

theorem Th102: :: JORDAN1A:102

for b₁, b₂ being Nat
for b₃ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₄, b₅ being Point of (TOP-REAL 2) st b₄ in W-most b₃ & b₅ in west_halfline b₄ & 1 <= b₁ & b₁ < len (Cage b₃,b₂) & b₅ in LSeg (Cage b₃,b₂),b₁ holds
LSeg (Cage b₃,b₂),b₁ is vertical

proof end;

theorem Th103: :: JORDAN1A:103

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in N-most b₂ & b₄ in (north_halfline b₃) /\ (L~ (Cage b₂,b₁)) holds
b₄ `2 = N-bound (L~ (Cage b₂,b₁))

proof end;

theorem Th104: :: JORDAN1A:104

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in E-most b₂ & b₄ in (east_halfline b₃) /\ (L~ (Cage b₂,b₁)) holds
b₄ `1 = E-bound (L~ (Cage b₂,b₁))

proof end;

theorem Th105: :: JORDAN1A:105

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in S-most b₂ & b₄ in (south_halfline b₃) /\ (L~ (Cage b₂,b₁)) holds
b₄ `2 = S-bound (L~ (Cage b₂,b₁))

proof end;

theorem Th106: :: JORDAN1A:106

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Point of (TOP-REAL 2) st b₃ in W-most b₂ & b₄ in (west_halfline b₃) /\ (L~ (Cage b₂,b₁)) holds
b₄ `1 = W-bound (L~ (Cage b₂,b₁))

proof end;

theorem Th107: :: JORDAN1A:107

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in N-most b₂ holds
ex b₄ being Point of (TOP-REAL 2) st (north_halfline b₃) /\ (L~ (Cage b₂,b₁)) = {b₄}

proof end;

theorem Th108: :: JORDAN1A:108

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in E-most b₂ holds
ex b₄ being Point of (TOP-REAL 2) st (east_halfline b₃) /\ (L~ (Cage b₂,b₁)) = {b₄}

proof end;

theorem Th109: :: JORDAN1A:109

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in S-most b₂ holds
ex b₄ being Point of (TOP-REAL 2) st (south_halfline b₃) /\ (L~ (Cage b₂,b₁)) = {b₄}

proof end;

theorem Th110: :: JORDAN1A:110

for b₁ being Nat
for b₂ being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being Point of (TOP-REAL 2) st b₃ in W-most b₂ holds
ex b₄ being Point of (TOP-REAL 2) st (west_halfline b₃) /\ (L~ (Cage b₂,b₁)) = {b₄}

proof end;