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

now

assume F <> {} ; :: thesis: contradiction
then consider A being Subset of such that
A4: A in F by SUBSET_1:10;
reconsider A = A as Subset of ;
( 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