let n be Element of NAT ; :: thesis: for V being Subset of (TOP-REAL n)
for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds
s1,s2,V -separate t2,t1
let V be Subset of (TOP-REAL n); :: thesis: for s1, s2, t1, t2 being Point of (TOP-REAL n) st s1,s2,V -separate t1,t2 holds
s1,s2,V -separate t2,t1
let s1, s2, t1, t2 be Point of (TOP-REAL n); :: thesis: ( s1,s2,V -separate t1,t2 implies s1,s2,V -separate t2,t1 )
assume A1: for A being Subset of (TOP-REAL n) st A is_an_arc_of s1,s2 & A c= V holds
A meets {t1,t2} ; :: according to JORDAN18:def 3 :: thesis: s1,s2,V -separate t2,t1
let A be Subset of (TOP-REAL n); :: according to JORDAN18:def 3 :: thesis: ( A is_an_arc_of s1,s2 & A c= V implies A meets {t2,t1} )
thus ( A is_an_arc_of s1,s2 & A c= V implies A meets {t2,t1} ) by A1; :: thesis: verum