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 is_an_arc_of p,q
let p, q be Point of (TOP-REAL 2); :: thesis: ( P is_S-P_arc_joining p,q implies P is_an_arc_of p,q )
assume P is_S-P_arc_joining p,q ; :: thesis: P is_an_arc_of p,q
then ex h being FinSequence of (TOP-REAL 2) st
( h is being_S-Seq & P = L~ h & p = h /. 1 & q = h /. (len h) ) by Def1;
hence P is_an_arc_of p,q by TOPREAL1:25; :: thesis: verum