let D be Simple_closed_curve; 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); ( 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
; ( 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
; ( 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 A3:
not
C is
trivial
;
( 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} )
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
and A5:
C c= D \ {p}
by SUBSET_1:44;
consider d1,
d2 being
Point of
(TOP-REAL 2) such that A6:
d1 in C
and A7:
d2 in C
and A8:
d1 <> d2
by A3, SUBSET_1:45;
reconsider Dp =
D \ {p} as non
empty Subset of
(TOP-REAL 2) by A5;
(TOP-REAL 2) | Dp,
I(01) are_homeomorphic
by A4, Th49;
then consider f being
Function of
((TOP-REAL 2) | Dp),
I(01) such that A9:
f is
being_homeomorphism
by T_0TOPSP:def 1;
reconsider C9 =
C as
Subset of
((TOP-REAL 2) | Dp) by A5, PRE_TOPC:8;
C c= [#] ((TOP-REAL 2) | Dp)
by A5, PRE_TOPC:8;
then A10:
C9 is
compact
by COMPTS_1:2;
set fC =
f .: C9;
A11:
C9 is
connected
by CONNSP_1:23;
A12:
rng f = [#] I(01)
by A9, TOPS_2:def 5;
f is
continuous
by A9, TOPS_2:def 5;
then reconsider fC =
f .: C9 as
connected compact Subset of
I(01) by A10, A11, A12, COMPTS_1:15, TOPS_2:61;
reconsider fC9 =
fC as
Subset of
I[01] by PRE_TOPC:11;
A13:
fC9 c= [#] I(01)
;
A14:
for
P being
Subset of
I(01) st
P = fC9 holds
P is
compact
;
d1 in D \ {p}
by A6, A5;
then
d1 in the
carrier of
((TOP-REAL 2) | Dp)
by PRE_TOPC:8;
then A15:
d1 in dom f
by FUNCT_2:def 1;
A16:
f is
one-to-one
by A9, TOPS_2:def 5;
d2 in D \ {p}
by A7, A5;
then
d2 in the
carrier of
((TOP-REAL 2) | Dp)
by PRE_TOPC:8;
then A17:
d2 in dom f
by FUNCT_2:def 1;
A18:
f . d2 in f .: C9
by A7, FUNCT_2:35;
then reconsider fC9 =
fC9 as non
empty connected compact Subset of
I[01] by A13, A14, COMPTS_1:2, CONNSP_1:23;
consider p1,
p2 being
Point of
I[01] such that A19:
p1 <= p2
and A20:
fC9 = [.p1,p2.]
by Th28;
A21:
f . d1 in f .: C9
by A6, FUNCT_2:35;
p1 <> p2
then
p1 < p2
by A19, XXREAL_0:1;
hence
( 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 A5, A9, A20, Th52;
verum end;