let GX be non empty TopSpace; :: thesis: for C being Subset of GX

for x being Point of GX st C is connected & Component_of x c= C holds

C = Component_of x

let C be Subset of GX; :: thesis: for x being Point of GX st C is connected & Component_of x c= C holds

C = Component_of x

let x be Point of GX; :: thesis: ( C is connected & Component_of x c= C implies C = Component_of x )

assume A1: C is connected ; :: thesis: ( not Component_of x c= C or C = Component_of x )

consider F being Subset-Family of GX such that

A2: for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) and

A3: Component_of x = union F by Def7;

assume A4: Component_of x c= C ; :: thesis: C = Component_of x

x in Component_of x by Th38;

then C in F by A1, A4, A2;

then C c= Component_of x by A3, ZFMISC_1:74;

hence C = Component_of x by A4; :: thesis: verum

for x being Point of GX st C is connected & Component_of x c= C holds

C = Component_of x

let C be Subset of GX; :: thesis: for x being Point of GX st C is connected & Component_of x c= C holds

C = Component_of x

let x be Point of GX; :: thesis: ( C is connected & Component_of x c= C implies C = Component_of x )

assume A1: C is connected ; :: thesis: ( not Component_of x c= C or C = Component_of x )

consider F being Subset-Family of GX such that

A2: for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) and

A3: Component_of x = union F by Def7;

assume A4: Component_of x c= C ; :: thesis: C = Component_of x

x in Component_of x by Th38;

then C in F by A1, A4, A2;

then C c= Component_of x by A3, ZFMISC_1:74;

hence C = Component_of x by A4; :: thesis: verum