theorem Th12: :: FINTOPO4:12

for FT being non empty filled RelStr
for IT being Subset of FT st FT is symmetric holds
( IT is connected iff for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT )