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