theorem Th6: :: FINTOPO4:6
for FT being non empty filled RelStr
for A, B being Subset of FT st A,B are_separated holds
A misses B by FIN_TOPO:13, XBOOLE_1:63;