theorem :: JORDAN18:24
for n being Element of NAT
for V being Subset of (TOP-REAL n)
for s1, s2, t being Point of (TOP-REAL n) holds t,t,V -separate s1,s2 by JORDAN6:37;