let P be Subset of (TOP-REAL 2); :: thesis: for p, q being Point of (TOP-REAL 2) st P is_S-P_arc_joining p,q holds
p <> q
let p, q be Point of (TOP-REAL 2); :: thesis: ( P is_S-P_arc_joining p,q implies p <> q )
assume that
A1: P is_S-P_arc_joining p,q and
A2: p = q ; :: thesis: contradiction
consider f being FinSequence of (TOP-REAL 2) such that
A3: f is being_S-Seq and
P = L~ f and
A4: ( p = f /. 1 & q = f /. (len f) ) by A1, Def1;
len f >= 2 by A3, TOPREAL1:def 8;
then ( Seg (len f) = dom f & len f >= 1 ) by FINSEQ_1:def 3, XXREAL_0:2;
then A5: ( len f in dom f & 1 in dom f ) by FINSEQ_1:1;
( f is one-to-one & 1 <> len f ) by A3, TOPREAL1:def 8;
hence contradiction by A2, A4, A5, PARTFUN2:10; :: thesis: verum