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 in P & q in P )
let p, q be Point of (TOP-REAL 2); :: thesis: ( P is_S-P_arc_joining p,q implies ( p in P & q in P ) )
assume P is_S-P_arc_joining p,q ; :: thesis: ( p in P & q in P )
then P is_an_arc_of p,q by Th2;
hence ( p in P & q in P ) by TOPREAL1:1; :: thesis: verum