let A1, A2 be Subset of (TOP-REAL 2); :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} holds
A1 <> A2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); :: thesis: ( A1 is_an_arc_of p1,p2 & A1 /\ A2 = {q1,q2} implies A1 <> A2 )
assume that
A1: A1 is_an_arc_of p1,p2 and
A2: A1 /\ A2 = {q1,q2} and
A3: A1 = A2 ; :: thesis: contradiction
consider p3 being Point of (TOP-REAL 2) such that
A4: p3 in A1 and
A5: ( p3 <> p1 & p3 <> p2 ) by A1, JORDAN6:55;
( p1 in A1 & p2 in A1 ) by A1, TOPREAL1:4;
then ( ( p1 = q1 or p1 = q2 ) & ( p2 = q1 or p2 = q2 ) & ( p3 = q1 or p3 = q2 ) ) by A2, A3, A4, TARSKI:def 2;
hence contradiction by A1, A5, JORDAN6:49; :: thesis: verum