theorem Th3: :: FINTOPO6:4

for FT being non empty RelStr
for A being Subset of FT st A is connected holds
for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated & not A2 = {} FT holds
B2 = {} FT