theorem :: FINTOPO6:26

for FT being non empty RelStr
for A being Subset of FT st A is_a_component_of FT holds
A <> {} FT