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 = {p1,p2} holds
A1 \/ A2 = C
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 = {p1,p2} holds
A1 \/ A2 = C
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 = {p1,p2} implies A1 \/ A2 = C )
assume that
A1: A1 is_an_arc_of p1,p2 and
A2: A2 is_an_arc_of p1,p2 and
A3: ( A1 c= C & A2 c= C ) and
A4: A1 /\ A2 = {p1,p2} ; :: thesis: A1 \/ A2 = C
A1 <> A2 by A2, A4, Th12;
hence A1 \/ A2 = C by A1, A2, A3, Th11; :: thesis: verum