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

( 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