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