theorem :: JORDAN18:25
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) st s1,s2,V -separate t1,t2 holds
s2,s1,V -separate t1,t2 by JORDAN5B:14;