theorem :: FINTOPO6:41

for FT being non empty RelStr
for A, B being Subset of FT st FT is filled & FT is symmetric & A is_a_component_of FT & B is_a_component_of FT & not A = B holds
A misses B by Th39, FINTOPO4:6;