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
s2,s1,V -separate t1,t2
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
s2,s1,V -separate t1,t2
let s1, s2, t1, t2 be Point of (TOP-REAL n); :: thesis: ( s1,s2,V -separate t1,t2 implies s2,s1,V -separate t1,t2 )
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: s2,s1,V -separate t1,t2
let A be Subset of (TOP-REAL n); :: according to JORDAN18:def 3 :: thesis: ( A is_an_arc_of s2,s1 & A c= V implies A meets {t1,t2} )
assume ( A is_an_arc_of s2,s1 & A c= V ) ; :: thesis: A meets {t1,t2}
hence A meets {t1,t2} by A1, JORDAN5B:14; :: thesis: verum