let D be Simple_closed_curve; :: thesis: for C being non empty connected compact Subset of (TOP-REAL 2) holds
( not C c= D or C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
let C be non empty connected compact Subset of (TOP-REAL 2); :: thesis: ( not C c= D or C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
assume A1:
C c= D
; :: thesis: ( C = D or ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
assume A2:
C <> D
; :: thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )
per cases
( C is trivial or not C is trivial )
;
suppose
not
C is
trivial
;
:: thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st C is_an_arc_of p1,p2 or ex p being Point of (TOP-REAL 2) st C = {p} )then consider d1,
d2 being
Point of
(TOP-REAL 2) such that A3:
(
d1 in C &
d2 in C &
d1 <> d2 )
by REALSET1:15;
C c< D
by A1, A2, XBOOLE_0:def 8;
then consider p being
Point of
(TOP-REAL 2) such that A4:
(
p in D &
C c= D \ {p} )
by Th1;
A5:
(
d1 in D \ {p} &
d2 in D \ {p} )
by A3, A4;
reconsider Dp =
D \ {p} as non
empty Subset of
(TOP-REAL 2) by A3, A4;
(TOP-REAL 2) | Dp,
I(01) are_homeomorphic
by A4, Th77;
then consider f being
Function of
((TOP-REAL 2) | Dp),
I(01) such that A6:
f is
being_homeomorphism
by T_0TOPSP:def 1;
reconsider C' =
C as
Subset of
((TOP-REAL 2) | Dp) by A4, PRE_TOPC:29;
set fC =
f .: C';
C c= [#] ((TOP-REAL 2) | Dp)
by A4, PRE_TOPC:29;
then A7:
C' is
compact
by COMPTS_1:11;
A8:
C' is
connected
by CONNSP_1:24;
A9:
f is
continuous
by A6, TOPS_2:def 5;
rng f = [#] I(01)
by A6, TOPS_2:def 5;
then reconsider fC =
f .: C' as
connected compact Subset of
I(01) by A7, A8, A9, COMPTS_1:24, TOPS_2:75;
reconsider fC' =
fC as
Subset of
I[01] by PRE_TOPC:39;
A10:
fC' c= [#] I(01)
;
A11:
for
P being
Subset of
I(01) st
P = fC' holds
P is
compact
;
A12:
d1 in the
carrier of
((TOP-REAL 2) | Dp)
by A5, PRE_TOPC:29;
A13:
f . d1 in f .: C'
by A3, FUNCT_2:43;
A14:
d2 in the
carrier of
((TOP-REAL 2) | Dp)
by A5, PRE_TOPC:29;
A15:
f . d2 in f .: C'
by A3, FUNCT_2:43;
then reconsider fC' =
fC' as non
empty connected compact Subset of
I[01] by A10, A11, COMPTS_1:11, CONNSP_1:24;
A16:
d1 in dom f
by A12, FUNCT_2:def 1;
A17:
d2 in dom f
by A14, FUNCT_2:def 1;
consider p1,
p2 being
Point of
I[01] such that A18:
(
p1 <= p2 &
fC' = [.p1,p2.] )
by Th56;
A19:
f is
one-to-one
by A6, TOPS_2:def 5;
p1 <> p2
then
p1 < p2
by A18, XXREAL_0:1;
then consider s1,
s2 being
Point of
(TOP-REAL 2) such that A22:
C is_an_arc_of s1,
s2
by A4, A6, A18, Th80;
thus
( ex
p1,
p2 being
Point of
(TOP-REAL 2) st
C is_an_arc_of p1,
p2 or ex
p being
Point of
(TOP-REAL 2) st
C = {p} )
by A22;
:: thesis: verum end;