let D be Simple_closed_curve; :: thesis:
let C be closed Subset of (TOP-REAL 2); :: thesis:
assume A1: C c< D ; :: thesis:
then A2: C c= D by XBOOLE_0:def 8;
A3: 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
A4: d1 in C and
A5: d2 in C and
A6: d1 <> d2 by SUBSET_1:45;
assume C c< D ; :: thesis:
then consider p being Point of (TOP-REAL 2) such that
A7: p in D and
A8: C c= D \ {p} by A4, SUBSET_1:44;
reconsider Dp = D \ {p} as non empty Subset of (TOP-REAL 2) by A4, A8;
(TOP-REAL 2) | Dp, I(01) are_homeomorphic by A7, 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;
d2 in D \ {p} by A5, A8;
then d2 in the carrier of ((TOP-REAL 2) | Dp) by PRE_TOPC:8;
then A10: d2 in dom f by FUNCT_2:def 1;
d1 in D \ {p} by A4, A8;
then d1 in the carrier of ((TOP-REAL 2) | Dp) by PRE_TOPC:8;
then A11: d1 in dom f by FUNCT_2:def 1;
A12: f is one-to-one by A9, TOPS_2:def 5;
C c= the carrier of ((TOP-REAL 2) | Dp) by A8, PRE_TOPC:8;
then A13: C c= dom f by FUNCT_2:def 1;
dom f = the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:def 1;
then A14: dom f c= the carrier of (TOP-REAL 2) by BORSUK_1:1;
dom f = the carrier of ((TOP-REAL 2) | Dp) by FUNCT_2:def 1;
then A15: dom f = Dp by PRE_TOPC:8;
reconsider C9 = C as Subset of ((TOP-REAL 2) | Dp) by A8, PRE_TOPC:8;
C c= [#] ((TOP-REAL 2) | Dp) by A8, PRE_TOPC:8;
then A16: C9 is compact by COMPTS_1:2;
set fC = f .: C9;
A17: 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 compact Subset of I(01) by A16, A17, COMPTS_1:15;
reconsider fC9 = fC as Subset of I[01] by PRE_TOPC:11;
A18: fC9 c= [#] I(01) ;
A19: for P being Subset of I(01) st P = fC9 holds
P is compact ;
fC9 c= the carrier of I(01) ;
then A20: fC9 c= ].0,1.[ by Def1;
A21: f . d2 in f .: C9 by A5, FUNCT_2:35;
then reconsider fC9 = fC9 as non empty compact Subset of I[01] by A18, A19, COMPTS_1:2;
consider p1, p2 being Point of I[01] such that
A22: p1 <= p2 and
A23: fC9 c= [.p1,p2.] and
A24: [.p1,p2.] c= ].0,1.[ by A20, Th55;
reconsider E = [.p1,p2.] as non empty connected compact Subset of I[01] by A22, Th21;
A25: f " E c= dom f by RELAT_1:132;
A26: f . d1 in f .: C9 by A4, FUNCT_2:35;
p1 <> p2

proof

assume p1 = p2 ; :: thesis:
then A27: fC9 c= {p1} by A23, XXREAL_1:17;
then A28: f . d2 = p1 by A21, TARSKI:def 1;
f . d1 = p1 by A26, A27, TARSKI:def 1;
hence contradiction by A6, A11, A10, A12, A28, FUNCT_1:def 4; :: thesis:

end;

then A29: p1 < p2 by A22, XXREAL_0:1;
E c= rng f by A17, A24, Def1;
then reconsider B = f " E as non empty Subset of (TOP-REAL 2) by A25, A14, RELAT_1:139, XBOOLE_1:1;
rng f = ].0,1.[ by A17, Def1;
then f .: (f " E) = E by A24, FUNCT_1:77;
then consider s1, s2 being Point of (TOP-REAL 2) such that
A30: B is_an_arc_of s1,s2 by A9, A29, A15, Th52, RELAT_1:132;
take s1 ; :: thesis:
take s2 ; :: thesis:
take B ; :: thesis:
thus B is_an_arc_of s1,s2 by A30; :: thesis:
Dp c= D by XBOOLE_1:36;
hence ( C c= B & B c= D ) by A23, A25, A15, A13, FUNCT_1:93; :: thesis:

end;

A31: C is compact by A2, RLTOPSP1:42, TOPREAL6:79;

per cases ;

suppose A32: C is trivial ; :: thesis:

per cases ;

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

consider p, q being Point of (TOP-REAL 2) such that
A34: p <> q and
A35: p in D and
A36: q in D by TOPREAL2:4;
reconsider CC = {p,q} as Subset of (TOP-REAL 2) ;
A37: q in CC by TARSKI:def 2;
p in CC by TARSKI:def 2;
then A38: not CC is trivial by A34, A37;
reconsider pp = {p}, qq = {q} as Subset of (TOP-REAL 2) ;
CC = pp \/ qq by ENUMSET1:1;
then A39: CC is compact by COMPTS_1:10;
A40: CC <> D

proof

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

end;

CC c= D by A35, A36, ZFMISC_1:32;
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
A41: B is_an_arc_of p1,p2 and
CC c= B and
A42: B c= D by A3, A38, A39;
take p1 ; :: thesis:
take p2 ; :: thesis:
take B ; :: thesis:
thus B is_an_arc_of p1,p2 by A41; :: thesis:
thus C c= B by A33; :: 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 A32, SUBSET_1:47;
consider y being Element of D such that
A44: x <> y by SUBSET_1:50;
reconsider y9 = y as Element of (TOP-REAL 2) ;
reconsider Y = {y9} as non empty compact Subset of (TOP-REAL 2) ;
reconsider Cy = C \/ Y as non empty compact Subset of (TOP-REAL 2) by A31, COMPTS_1:10;
A45: x in C by A43, TARSKI:def 1;
A46: Cy <> D

proof

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

end;

{y} c= D ;
then Cy c= D by A2, XBOOLE_1:8;
then A48: Cy c< D by A46, XBOOLE_0:def 8;
A49: C c= Cy by XBOOLE_1:7;
y in Y by TARSKI:def 1;
then y in Cy by XBOOLE_0:def 3;
then not Cy is trivial by A45, A44, A49;
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 and
A51: Cy c= B and
A52: B c= D by A3, A48;
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 A49, A51; :: thesis:
thus B c= D by A52; :: 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, A31, A3; :: thesis:

end;