:: deftheorem defines is_an_arc_of TOPREAL1:def 1 :
for T being TopSpace
for p1, p2 being Point of T
for P being Subset of T holds
( P is_an_arc_of p1,p2 iff ex f being Function of I[01],(T | P) st
( f is being_homeomorphism & f . 0 = p1 & f . 1 = p2 ) );