let GX be non empty TopSpace; :: thesis: for A being Subset of GX holds
( A is_a_component_of GX iff ex x being Point of GX st A = Component_of x )
let A be Subset of GX; :: thesis: ( A is_a_component_of GX iff ex x being Point of GX st A = Component_of x )

A1: now

assume A2: A is_a_component_of GX ; :: thesis: ex x being Point of GX st A = Component_of x
then A <> {} GX by Th34;
then consider y being Point of GX such that
A3: y in A by PRE_TOPC:41;
take x = y; :: thesis: A = Component_of x
consider F being Subset-Family of GX such that
A4: for B being Subset of GX holds
( B in F iff ( B is connected & x in B ) ) and
A5: union F = Component_of x by Def7;
A6: Component_of x is connected by Th41;
A is connected by A2, Def5;
then A in F by A3, A4;
then A c= union F by ZFMISC_1:92;
hence A = Component_of x by A2, A5, A6, Def5; :: thesis: verum

end;

now

given x being Point of GX such that A7: A = Component_of x ; :: thesis: A is_a_component_of GX
A8: for B being Subset of GX st B is connected & A c= B holds
A = B by A7, Th42;
A is connected by A7, Th41;
hence A is_a_component_of GX by A8, Def5; :: thesis: verum

end;

hence ( A is_a_component_of GX iff ex x being Point of GX st A = Component_of x ) by A1; :: thesis: verum