:: JORDAN1E semantic presentation

theorem Th1: :: JORDAN1E:1

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being compact Subset of (TOP-REAL 2) st b₁ c= b₂ holds
N-bound b₁ <= N-bound b₂

proof end;

theorem Th2: :: JORDAN1E:2

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being compact Subset of (TOP-REAL 2) st b₁ c= b₂ holds
E-bound b₁ <= E-bound b₂

proof end;

theorem Th3: :: JORDAN1E:3

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being compact Subset of (TOP-REAL 2) st b₁ c= b₂ holds
S-bound b₁ >= S-bound b₂

proof end;

theorem Th4: :: JORDAN1E:4

for b₁ being non empty Subset of (TOP-REAL 2)
for b₂ being compact Subset of (TOP-REAL 2) st b₁ c= b₂ holds
W-bound b₁ >= W-bound b₂

proof end;

theorem Th5: :: JORDAN1E:5

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is_in_the_area_of b₂ holds
for b₃ being Element of (TOP-REAL 2) st b₃ in rng b₁ holds
b₁ -: b₃ is_in_the_area_of b₂

proof end;

theorem Th6: :: JORDAN1E:6

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₁ is_in_the_area_of b₂ holds
for b₃ being Element of (TOP-REAL 2) st b₃ in rng b₁ holds
b₁ :- b₃ is_in_the_area_of b₂

proof end;

theorem Th7: :: JORDAN1E:7

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
L_Cut b₁,b₂ <> {}

proof end;

theorem Th8: :: JORDAN1E:8

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ & len (R_Cut b₁,b₂) >= 2 holds
b₁ . 1 in L~ (R_Cut b₁,b₂)

proof end;

theorem Th9: :: JORDAN1E:9

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is_S-Seq holds
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ holds
not b₁ . 1 in L~ (mid b₁,((Index b₂,b₁) + 1),(len b₁))

proof end;

theorem Th10: :: JORDAN1E:10

for b₁, b₂, b₃, b₄ being Nat st b₁ + b₂ = b₃ + b₄ & b₁ <= b₃ & b₂ <= b₄ holds
b₁ = b₃

proof end;

theorem Th11: :: JORDAN1E:11

for b₁ being FinSequence of (TOP-REAL 2) st b₁ is_S-Seq holds
for b₂ being Point of (TOP-REAL 2) st b₂ in L~ b₁ & b₁ . 1 in L~ (L_Cut b₁,b₂) holds
b₁ . 1 = b₂

proof end;

definition

let c₁ be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c₂ be Nat;
func Upper_Seq c₁,c₂ -> FinSequence of (TOP-REAL 2) equals :: JORDAN1E:def 1
(Rotate (Cage a₁,a₂),(W-min (L~ (Cage a₁,a₂)))) -: (E-max (L~ (Cage a₁,a₂)));
coherence ;

end;

:: deftheorem Def1 defines Upper_Seq JORDAN1E:def 1 :

theorem Th12: :: JORDAN1E:12

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds len (Upper_Seq b₁,b₂) = (E-max (L~ (Cage b₁,b₂))) .. (Rotate (Cage b₁,b₂),(W-min (L~ (Cage b₁,b₂))))

proof end;

definition

let c₁ be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c₂ be Nat;
func Lower_Seq c₁,c₂ -> FinSequence of (TOP-REAL 2) equals :: JORDAN1E:def 2
(Rotate (Cage a₁,a₂),(W-min (L~ (Cage a₁,a₂)))) :- (E-max (L~ (Cage a₁,a₂)));
coherence ;

end;

:: deftheorem Def2 defines Lower_Seq JORDAN1E:def 2 :

theorem Th13: :: JORDAN1E:13

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds len (Lower_Seq b₁,b₂) = ((len (Rotate (Cage b₁,b₂),(W-min (L~ (Cage b₁,b₂))))) - ((E-max (L~ (Cage b₁,b₂))) .. (Rotate (Cage b₁,b₂),(W-min (L~ (Cage b₁,b₂)))))) + 1

proof end;

registration

let c₁ be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c₂ be Nat;
cluster Upper_Seq a₁,a₂ -> non empty ;
coherence

proof end;

cluster Lower_Seq a₁,a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c₂ be Nat;
cluster Upper_Seq a₁,a₂ -> non empty one-to-one special unfolded s.n.c. ;
coherence

proof end;

cluster Lower_Seq a₁,a₂ -> non empty one-to-one special unfolded s.n.c. ;
coherence

proof end;

end;

theorem Th14: :: JORDAN1E:14

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds (len (Upper_Seq b₁,b₂)) + (len (Lower_Seq b₁,b₂)) = (len (Cage b₁,b₂)) + 1

proof end;

theorem Th15: :: JORDAN1E:15

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds Rotate (Cage b₁,b₂),(W-min (L~ (Cage b₁,b₂))) = (Upper_Seq b₁,b₂) ^' (Lower_Seq b₁,b₂)

proof end;

theorem Th16: :: JORDAN1E:16

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds L~ (Cage b₁,b₂) = L~ ((Upper_Seq b₁,b₂) ^' (Lower_Seq b₁,b₂))

proof end;

theorem Th17: :: JORDAN1E:17

for b₁ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds L~ (Cage b₁,b₂) = (L~ (Upper_Seq b₁,b₂)) \/ (L~ (Lower_Seq b₁,b₂))

proof end;

theorem Th18: :: JORDAN1E:18

for b₁ being Simple_closed_curve holds W-min b₁ <> E-min b₁

proof end;

theorem Th19: :: JORDAN1E:19

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds
( len (Upper_Seq b₁,b₂) >= 3 & len (Lower_Seq b₁,b₂) >= 3 )

proof end;

registration

let c₁ be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c₂ be Nat;
cluster Upper_Seq a₁,a₂ -> non empty one-to-one special unfolded s.n.c. being_S-Seq ;
coherence

proof end;

cluster Lower_Seq a₁,a₂ -> non empty one-to-one special unfolded s.n.c. being_S-Seq ;
coherence

proof end;

end;

theorem Th20: :: JORDAN1E:20

for b₁ being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₂ being Nat holds (L~ (Upper_Seq b₁,b₂)) /\ (L~ (Lower_Seq b₁,b₂)) = {(W-min (L~ (Cage b₁,b₂))),(E-max (L~ (Cage b₁,b₂)))}

proof end;

theorem Th21: :: JORDAN1E:21

for b₁ being Nat
for b₂ being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq b₂,b₁ is_in_the_area_of Cage b₂,b₁

proof end;

theorem Th22: :: JORDAN1E:22

for b₁ being Nat
for b₂ being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq b₂,b₁ is_in_the_area_of Cage b₂,b₁

proof end;

theorem Th23: :: JORDAN1E:23

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

proof end;

theorem Th24: :: JORDAN1E:24

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

proof end;

theorem Th25: :: JORDAN1E:25

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

proof end;

theorem Th26: :: JORDAN1E:26

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

proof end;