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} )

A3: p1 <> p2 by A1, JORDAN6:37;

( p1 in P & p2 in P ) by A1, TOPREAL1:1;

then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that

A4: P1 is_an_arc_of p1,p2 and

A5: P2 is_an_arc_of p1,p2 and

A6: C = P1 \/ P2 and

A7: P1 /\ P2 = {p1,p2} by A2, A3, TOPREAL2:5;

reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;

A8: ( P1 c= C & P2 c= C ) by A6, XBOOLE_1:7;

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} )

A3: p1 <> p2 by A1, JORDAN6:37;

( p1 in P & p2 in P ) by A1, TOPREAL1:1;

then consider P1, P2 being non empty Subset of (TOP-REAL 2) such that

A4: P1 is_an_arc_of p1,p2 and

A5: P2 is_an_arc_of p1,p2 and

A6: C = P1 \/ P2 and

A7: P1 /\ P2 = {p1,p2} by A2, A3, TOPREAL2:5;

reconsider P1 = P1, P2 = P2 as non empty Subset of (TOP-REAL 2) ;

A8: ( P1 c= C & P2 c= C ) by A6, XBOOLE_1:7;

A9: now :: thesis: not P1 = P2

assume A10:
P1 = P2
; :: thesis: contradiction

ex p3 being Point of (TOP-REAL 2) st

( p3 in P1 & p3 <> p1 & p3 <> p2 ) by A4, JORDAN6:42;

hence contradiction by A7, A10, TARSKI:def 2; :: thesis: verum

end;ex p3 being Point of (TOP-REAL 2) st

( p3 in P1 & p3 <> p1 & p3 <> p2 ) by A4, JORDAN6:42;

hence contradiction by A7, A10, TARSKI:def 2; :: thesis: verum

per cases
( P = P1 or P = P2 )
by A1, A2, A4, A5, A8, A9, JORDAN16:14;

end;

suppose A11:
P = P1
; :: 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} )

( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )

take
P2
; :: thesis: ( P2 is_an_arc_of p1,p2 & P \/ P2 = C & P /\ P2 = {p1,p2} )

thus ( P2 is_an_arc_of p1,p2 & P \/ P2 = C & P /\ P2 = {p1,p2} ) by A5, A6, A7, A11; :: thesis: verum

end;thus ( P2 is_an_arc_of p1,p2 & P \/ P2 = C & P /\ P2 = {p1,p2} ) by A5, A6, A7, A11; :: thesis: verum

suppose A12:
P = P2
; :: 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} )

( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )

take
P1
; :: thesis: ( P1 is_an_arc_of p1,p2 & P \/ P1 = C & P /\ P1 = {p1,p2} )

thus ( P1 is_an_arc_of p1,p2 & P \/ P1 = C & P /\ P1 = {p1,p2} ) by A4, A6, A7, A12; :: thesis: verum

end;thus ( P1 is_an_arc_of p1,p2 & P \/ P1 = C & P /\ P1 = {p1,p2} ) by A4, A6, A7, A12; :: thesis: verum