:: deftheorem defines is_a_component_of FINTOPO6:def 4 :
for FT being non empty RelStr
for A being Subset of FT holds
( A is_a_component_of FT iff ( A is connected & ( for B being Subset of FT st B is connected & A c= B holds
A = B ) ) );