theorem :: FINTOPO6:27

for FT being non empty RelStr
for A, B being Subset of FT st A is closed & B is closed & A misses B holds
A,B are_separated by FINTOPO4:def 1;