let GX be TopSpace; :: thesis: for V being Subset of GX st ( for A being Subset of GX holds
( not A is connected or not V c= A ) ) holds
Component_of V = {}
let V be Subset of GX; :: thesis: ( ( for A being Subset of GX holds
( not A is connected or not V c= A ) ) implies Component_of V = {} )
assume A1: for A being Subset of GX holds
( not A is connected or not V c= A ) ; :: thesis: Component_of V = {}
consider F being Subset-Family of GX such that
A2: for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) and
A3: Component_of V = union F by Def1;

now :: thesis: not F <> {}

assume F <> {} ; :: thesis: contradiction
then consider A being Subset of GX such that
A4: A in F by SUBSET_1:4;
reconsider A = A as Subset of GX ;
( A is connected & V c= A ) by A2, A4;
hence contradiction by A1; :: thesis: verum

end;

hence Component_of V = {} by A3, ZFMISC_1:2; :: thesis: verum