:: deftheorem defines is_S-P_arc_joining TOPREAL4:def 1 :
for P being Subset of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) holds
( P is_S-P_arc_joining p,q iff ex f being FinSequence of (TOP-REAL 2) st
( f is being_S-Seq & P = L~ f & p = f /. 1 & q = f /. (len f) ) );