let P be Subset of (TOP-REAL 2); :: thesis: ( P is being_S-P_arc implies ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2 )
assume P is being_S-P_arc ; :: thesis: ex p1, p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2
then consider h being FinSequence of (TOP-REAL 2) such that
A1: h is being_S-Seq and
A2: P = L~ h by Def11;
take p1 = h /. 1; :: thesis: ex p2 being Point of (TOP-REAL 2) st P is_an_arc_of p1,p2
take p2 = h /. (len h); :: thesis: P is_an_arc_of p1,p2
thus P is_an_arc_of p1,p2 by A1, A2, Th31; :: thesis: verum