let C be Simple_closed_curve; :: thesis: for P being Subset of (TOP-REAL 2)
for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( P is_an_arc_of p1,p2 & P c= C implies ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} ) )
assume that
A1:
P is_an_arc_of p1,p2
and
A2:
P c= C
; :: thesis: ex R being non empty Subset of (TOP-REAL 2) st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )
( p1 in P & p2 in P )
by A1, TOPREAL1:4;
then
( p1 <> p2 & p1 in C & p2 in C )
by A1, A2, JORDAN6:49;
then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that
A3:
P1 is_an_arc_of p1,p2
and
A4:
P2 is_an_arc_of p1,p2
and
A5:
C = P1 \/ P2
and
A6:
P1 /\ P2 = {p1,p2}
by TOPREAL2:5;
reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;
A7:
( P1 c= C & P2 c= C )
by A5, XBOOLE_1:7;