:: deftheorem defines a_component CONNSP_1:def 5 :
for GX being TopStruct
for A being Subset of GX holds
( A is a_component iff ( A is connected & ( for B being Subset of GX st B is connected & A c= B holds
A = B ) ) );