:: deftheorem defines -separate JORDAN18:def 3 :
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for s1, s2, t1, t2 being Point of (TOP-REAL n) holds
( s1,s2,V -separate t1,t2 iff for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds
A meets {t1,t2} );