:: JORDAN22 semantic presentation

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

Lm2: for r being real number
for X being Subset of (TOP-REAL 2) st r in proj2 .: X holds
ex x being Point of (TOP-REAL 2) st
( x in X & proj2 . x = r )

proof end;

theorem Th1: :: JORDAN22:1

for C being Simple_closed_curve
for i being Nat holds (Upper_Appr C) . i c= Cl (RightComp (Cage C,0))

proof end;

theorem Th2: :: JORDAN22:2

for C being Simple_closed_curve
for i being Nat holds (Lower_Appr C) . i c= Cl (RightComp (Cage C,0))

proof end;

registration

let C be Simple_closed_curve;
cluster Upper_Arc C -> connected ;
coherence

proof end;

cluster Lower_Arc C -> connected ;
coherence

proof end;

end;

theorem :: JORDAN22:3

for C being Simple_closed_curve
for i being Nat holds
( (Upper_Appr C) . i is compact & (Upper_Appr C) . i is connected )

proof end;

theorem :: JORDAN22:4

for C being Simple_closed_curve
for i being Nat holds
( (Lower_Appr C) . i is compact & (Lower_Appr C) . i is connected )

proof end;

registration

let C be Simple_closed_curve;
cluster North_Arc C -> compact ;
coherence

proof end;

cluster South_Arc C -> compact ;
coherence

proof end;

end;

theorem :: JORDAN22:5

for C being Simple_closed_curve holds W-min C in North_Arc C

proof end;

theorem :: JORDAN22:6

for C being Simple_closed_curve holds E-max C in North_Arc C

proof end;

theorem :: JORDAN22:7

for C being Simple_closed_curve holds W-min C in South_Arc C

proof end;

theorem :: JORDAN22:8

for C being Simple_closed_curve holds E-max C in South_Arc C

proof end;

theorem Th9: :: JORDAN22:9

for C being Simple_closed_curve holds UMP C in North_Arc C

proof end;

theorem Th10: :: JORDAN22:10

for C being Simple_closed_curve holds LMP C in South_Arc C

proof end;

theorem Th11: :: JORDAN22:11

for C being Simple_closed_curve holds North_Arc C c= C

proof end;

theorem Th12: :: JORDAN22:12

for C being Simple_closed_curve holds South_Arc C c= C

proof end;

theorem :: JORDAN22:13

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

proof end;