let C be Simple_closed_curve; :: thesis: for P being Subset of ()
for p1, p2 being Point of () st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of () st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )

let P be Subset of (); :: thesis: for p1, p2 being Point of () st P is_an_arc_of p1,p2 & P c= C holds
ex R being non empty Subset of () st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )

let p1, p2 be Point of (); :: thesis: ( P is_an_arc_of p1,p2 & P c= C implies ex R being non empty Subset of () 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 () st
( R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,p2} )

A3: p1 <> p2 by ;
( p1 in P & p2 in P ) by ;
then consider P1, P2 being non empty Subset of () 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 ;
reconsider P1 = P1, P2 = P2 as non empty Subset of () ;
A8: ( P1 c= C & P2 c= C ) by ;
A9: now :: thesis: not P1 = P2
assume A10: P1 = P2 ; :: thesis: contradiction
ex p3 being Point of () st
( p3 in P1 & p3 <> p1 & p3 <> p2 ) by ;
hence contradiction by A7, A10, TARSKI:def 2; :: thesis: verum
end;
per cases ( P = P1 or P = P2 ) by A1, A2, A4, A5, A8, A9, JORDAN16:14;
suppose A11: P = P1 ; :: thesis: ex R being non empty Subset of () st
( 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;
suppose A12: P = P2 ; :: thesis: ex R being non empty Subset of () st
( 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;
end;