theorem :: FINTOPO6:17

for FT being non empty filled RelStr
for A being non empty Subset of FT st FT is symmetric holds
( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT )