let D be Simple_closed_curve; :: thesis:
let C be closed Subset of (TOP-REAL 2); :: thesis:
assume A1: C c< D ; :: thesis:
then X: C c= D by XBOOLE_0:def 8;
D is Bounded by JORDAN2C:73;
then A2: C is compact by X, JORDAN2C:16, TOPREAL6:88;
A4: for C being compact Subset of (TOP-REAL 2) st not C is trivial & C c< D holds
ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D )

proof

let C be compact Subset of (TOP-REAL 2); :: thesis:
assume not C is trivial ; :: thesis:
then consider d1, d2 being Point of (TOP-REAL 2) such that
A5: ( d1 in C & d2 in C & d1 <> d2 ) by REALSET1:15;
assume C c< D ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A7: ( p in D & C c= D \ {p} ) by A5, Th1;
A8: ( d1 in D \ {p} & d2 in D \ {p} ) by A5, A7;
reconsider Dp = D \ {p} as non empty Subset of (TOP-REAL 2) by A5, A7;
(TOP-REAL 2) | Dp, I(01) are_homeomorphic by A7, Th77;
then consider f being Function of ((TOP-REAL 2) | Dp),I(01) such that
A9: f is being_homeomorphism by T_0TOPSP:def 1;
A10: C c= the carrier of ((TOP-REAL 2) | Dp) by A7, PRE_TOPC:29;
reconsider C' = C as Subset of ((TOP-REAL 2) | Dp) by A7, PRE_TOPC:29;
set fC = f .: C';
C c= [#] ((TOP-REAL 2) | Dp) by A7, PRE_TOPC:29;
then A11: C' is compact by COMPTS_1:11;
A12: f is continuous by A9, TOPS_2:def 5;
A13: rng f = [#] I(01) by A9, TOPS_2:def 5;
then reconsider fC = f .: C' as compact Subset of I(01) by A11, A12, COMPTS_1:24;
reconsider fC' = fC as Subset of I[01] by PRE_TOPC:39;
A14: fC' c= the carrier of I(01) ;
A15: fC' c= [#] I(01) ;
A16: fC' c= ].0 ,1.[ by A14, Def1;
A17: for P being Subset of I(01) st P = fC' holds
P is compact ;
A18: d1 in the carrier of ((TOP-REAL 2) | Dp) by A8, PRE_TOPC:29;
A19: f . d1 in f .: C' by A5, FUNCT_2:43;
A20: d2 in the carrier of ((TOP-REAL 2) | Dp) by A8, PRE_TOPC:29;
A21: f . d2 in f .: C' by A5, FUNCT_2:43;
then reconsider fC' = fC' as non empty compact Subset of I[01] by A15, A17, COMPTS_1:11;
A22: d1 in dom f by A18, FUNCT_2:def 1;
A23: d2 in dom f by A20, FUNCT_2:def 1;
consider p1, p2 being Point of I[01] such that
A24: ( p1 <= p2 & fC' c= [.p1,p2.] & [.p1,p2.] c= ].0 ,1.[ ) by A16, Th83;
reconsider E = [.p1,p2.] as non empty connected compact Subset of I[01] by A24, Th49;
A25: f is one-to-one by A9, TOPS_2:def 5;
p1 <> p2

proof

assume p1 = p2 ; :: thesis:
then A26: fC' c= {p1} by A24, XXREAL_1:17;
then A27: f . d1 = p1 by A19, TARSKI:def 1;
f . d2 = p1 by A21, A26, TARSKI:def 1;
hence contradiction by A5, A22, A23, A25, A27, FUNCT_1:def 8; :: thesis:

end;

then A28: p1 < p2 by A24, XXREAL_0:1;
A29: rng f = ].0 ,1.[ by A13, Def1;
A30: E c= rng f by A13, A24, Def1;
A31: f " E c= dom f by RELAT_1:167;
dom f = the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:def 1;
then dom f c= the carrier of (TOP-REAL 2) by BORSUK_1:35;
then reconsider B = f " E as non empty Subset of (TOP-REAL 2) by A30, A31, RELAT_1:174, XBOOLE_1:1;
dom f = the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:def 1;
then A32: dom f = Dp by PRE_TOPC:29;
A33: Dp c= D by XBOOLE_1:36;
f .: (f " E) = E by A24, A29, FUNCT_1:147;
then consider s1, s2 being Point of (TOP-REAL 2) such that
A34: B is_an_arc_of s1,s2 by A9, A28, A31, A32, Th80;
take s1 ; :: thesis:
take s2 ; :: thesis:
take B ; :: thesis:
thus B is_an_arc_of s1,s2 by A34; :: thesis:
C c= dom f by A10, FUNCT_2:def 1;
hence ( C c= B & B c= D ) by A24, A31, A32, A33, FUNCT_1:163, XBOOLE_1:1; :: thesis:

end;

per cases ;

suppose A35: C is trivial ; :: thesis:

per cases ;

suppose A36: C = {} ; :: thesis:

consider p, q being Point of (TOP-REAL 2) such that
A37: ( p <> q & p in D & q in D ) by TOPREAL2:4;
reconsider CC = {p,q} as Subset of (TOP-REAL 2) ;
( p in CC & q in CC ) by TARSKI:def 2;
then A38: not CC is trivial by A37, REALSET1:14;
reconsider pp = {p}, qq = {q} as Subset of (TOP-REAL 2) ;
CC = pp \/ qq by ENUMSET1:41;
then A39: CC is compact by COMPTS_1:19;
A40: CC c= D by A37, ZFMISC_1:38;
CC <> D

proof

assume CC = D ; :: thesis:
then A41: D \ CC = {} by XBOOLE_1:37;
not {} ((TOP-REAL 2) | D) is connected by A37, A41, JORDAN6:60;
hence contradiction ; :: thesis:

end;

then CC c< D by A40, XBOOLE_0:def 8;
then consider p1, p2 being Point of (TOP-REAL 2), B being Subset of (TOP-REAL 2) such that
A42: ( B is_an_arc_of p1,p2 & CC c= B & B c= D ) by A4, A38, A39;
take p1 ; :: thesis:
take p2 ; :: thesis:
take B ; :: thesis:
thus B is_an_arc_of p1,p2 by A42; :: thesis:
thus C c= B by A36, XBOOLE_1:2; :: thesis:
thus B c= D by A42; :: thesis:

end;

suppose C <> {} ; :: thesis:

then consider x being Element of (TOP-REAL 2) such that
A43: C = {x} by A35, Th2;
A44: x in C by A43, TARSKI:def 1;
consider y being Element of D such that
A45: x <> y by Th3;
reconsider y' = y as Element of (TOP-REAL 2) ;
reconsider Y = {y'} as non empty compact Subset of (TOP-REAL 2) ;
reconsider Cy = C \/ Y as non empty compact Subset of (TOP-REAL 2) by A2, COMPTS_1:19;
A46: C c= Cy by XBOOLE_1:7;
y in Y by TARSKI:def 1;
then y in Cy by XBOOLE_0:def 3;
then A47: not Cy is trivial by A44, A45, A46, REALSET1:14;
{y} c= D ;
then A48: Cy c= D by X, XBOOLE_1:8;
Cy <> D

proof

assume Cy = D ; :: thesis:
then A49: D \ Cy = {} by XBOOLE_1:37;
Cy = {x,y} by A43, ENUMSET1:41;
then not {} ((TOP-REAL 2) | D) is connected by X, A44, A45, A49, JORDAN6:60;
hence contradiction ; :: thesis:

end;

then Cy c< D by A48, XBOOLE_0:def 8;
then consider p1, p2 being Point of (TOP-REAL 2), B being Subset of (TOP-REAL 2) such that
A50: ( B is_an_arc_of p1,p2 & Cy c= B & B c= D ) by A4, A47;
take p1 ; :: thesis:
take p2 ; :: thesis:
take B ; :: thesis:
thus B is_an_arc_of p1,p2 by A50; :: thesis:
thus C c= B by A46, A50, XBOOLE_1:1; :: thesis:
thus B c= D by A50; :: thesis:

end;

suppose not C is trivial ; :: thesis:

hence ex p1, p2 being Point of (TOP-REAL 2) ex B being Subset of (TOP-REAL 2) st
( B is_an_arc_of p1,p2 & C c= B & B c= D ) by A1, A2, A4; :: thesis:

end;