let n be Element of NAT ; :: thesis: for V being Subset of (TOP-REAL n)
for t, s1, s2 being Point of (TOP-REAL n) holds t,t,V -separate s1,s2
let V be Subset of (TOP-REAL n); :: thesis: for t, s1, s2 being Point of (TOP-REAL n) holds t,t,V -separate s1,s2
let t, s1, s2 be Point of (TOP-REAL n); :: thesis: t,t,V -separate s1,s2
assume not t,t,V -separate s1,s2 ; :: thesis: contradiction
then ex A being Subset of (TOP-REAL n) st
( A is_an_arc_of t,t & A c= V & A misses {s1,s2} ) by Def3;
hence contradiction by JORDAN6:49; :: thesis: verum