theorem :: CONNSP_1:13

for GX being TopSpace holds
( GX is connected iff for A being Subset of GX st A is open & A is closed & not A = {} GX holds
A = [#] GX )