:: deftheorem defines is_a_component_of FINTOPO6:def 5 :
for FT being non empty RelStr
for A being non empty Subset of FT
for B being Subset of FT holds
( B is_a_component_of A iff ex B1 being Subset of (FT | A) st
( B1 = B & B1 is_a_component_of FT | A ) );