:: JORDAN22 semantic presentation

Lemma1: TOP-REAL 2 = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;

Lemma2: for b₁ being real number
for b₂ being Subset of (TOP-REAL 2) st b₁ in proj2 .: b₂ holds
ex b₃ being Point of (TOP-REAL 2) st
( b₃ in b₂ & proj2 . b₃ = b₁ )

proof end;

theorem Th1: :: JORDAN22:1

for b₁ being Simple_closed_curve
for b₂ being Nat holds (Upper_Appr b₁) . b₂ c= Cl (RightComp (Cage b₁,0))

proof end;

theorem Th2: :: JORDAN22:2

for b₁ being Simple_closed_curve
for b₂ being Nat holds (Lower_Appr b₁) . b₂ c= Cl (RightComp (Cage b₁,0))

proof end;

registration

let c₁ be Simple_closed_curve;
cluster Upper_Arc a₁ -> connected ;
coherence

proof end;

cluster Lower_Arc a₁ -> connected ;
coherence

proof end;

end;

theorem Th3: :: JORDAN22:3

for b₁ being Simple_closed_curve
for b₂ being Nat holds
( (Upper_Appr b₁) . b₂ is compact & (Upper_Appr b₁) . b₂ is connected )

proof end;

theorem Th4: :: JORDAN22:4

for b₁ being Simple_closed_curve
for b₂ being Nat holds
( (Lower_Appr b₁) . b₂ is compact & (Lower_Appr b₁) . b₂ is connected )

proof end;

registration

let c₁ be Simple_closed_curve;
cluster North_Arc a₁ -> compact ;
coherence

proof end;

cluster South_Arc a₁ -> compact ;
coherence

proof end;

end;

theorem Th5: :: JORDAN22:5

for b₁ being Simple_closed_curve holds W-min b₁ in North_Arc b₁

proof end;

theorem Th6: :: JORDAN22:6

for b₁ being Simple_closed_curve holds E-max b₁ in North_Arc b₁

proof end;

theorem Th7: :: JORDAN22:7

for b₁ being Simple_closed_curve holds W-min b₁ in South_Arc b₁

proof end;

theorem Th8: :: JORDAN22:8

for b₁ being Simple_closed_curve holds E-max b₁ in South_Arc b₁

proof end;

theorem Th9: :: JORDAN22:9

for b₁ being Simple_closed_curve holds UMP b₁ in North_Arc b₁

proof end;

theorem Th10: :: JORDAN22:10

for b₁ being Simple_closed_curve holds LMP b₁ in South_Arc b₁

proof end;

theorem Th11: :: JORDAN22:11

for b₁ being Simple_closed_curve holds North_Arc b₁ c= b₁

proof end;

theorem Th12: :: JORDAN22:12

for b₁ being Simple_closed_curve holds South_Arc b₁ c= b₁

proof end;

theorem Th13: :: JORDAN22:13

for b₁ being Simple_closed_curve holds
( ( LMP b₁ in Lower_Arc b₁ & UMP b₁ in Upper_Arc b₁ ) or ( UMP b₁ in Lower_Arc b₁ & LMP b₁ in Upper_Arc b₁ ) )

proof end;