theorem Th4: :: FINTOPO6:5

for FT being non empty RelStr st FT is connected holds
for A, B being Subset of FT st [#] FT = A \/ B & A misses B & A,B are_separated & not A = {} FT holds
B = {} FT