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;

( 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 <> {}

hence
Component_of V = {}
by A3, ZFMISC_1:2; :: thesis: verumassume
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;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