:: deftheorem Def3 defines connected CONNSP_1:def 3 :
for GX being TopStruct
for A being Subset of GX holds
( A is connected iff GX | A is connected );