:: deftheorem defines is_a_component_of CONNSP_1:def 6 :
for GX being TopStruct
for A, B being Subset of GX holds
( B is_a_component_of A iff ex B1 being Subset of (GX | A) st
( B1 = B & B1 is a_component ) );