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} & A1 = A2 ) ; :: thesis: contradiction
p1 in A1 by A1, TOPREAL1:1;
then A3: ( p1 = q1 or p1 = q2 ) by A2, TARSKI:def 2;
p2 in A1 by A1, TOPREAL1:1;
then A4: ( p2 = q1 or p2 = q2 ) by A2, TARSKI:def 2;
ex p3 being Point of (TOP-REAL 2) st
( p3 in A1 & p3 <> p1 & p3 <> p2 ) by A1, JORDAN6:42;
hence contradiction by A1, A2, A3, A4, JORDAN6:37, TARSKI:def 2; :: thesis: verum