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 ;
take h /. 1 ; :: thesis: ex p2 being Point of (TOP-REAL 2) st P is_an_arc_of h /. 1,p2
take h /. (len h) ; :: thesis: P is_an_arc_of h /. 1,h /. (len h)
thus P is_an_arc_of h /. 1,h /. (len h) by A1, A2, Th25; :: thesis: verum