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