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 )
assume A2: Component_of x c= C ; :: thesis: C = Component_of x
consider F being Subset-Family of GX such that
A3: for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) and
A4: Component_of x = union F by Def7;
x in Component_of x by Th40;
then C in F by A1, A2, A3;
then C c= Component_of x by A4, ZFMISC_1:92;
hence C = Component_of x by A2, XBOOLE_0:def 10; :: thesis: verum