:: deftheorem defines connected CONNSP_1:def 2 :
for GX being TopStruct holds
( GX is connected iff for A, B being Subset of GX st [#] GX = A \/ B & A,B are_separated & not A = {} GX holds
B = {} GX );