let GX be non empty TopSpace; :: thesis: for A being Subset of GX holds
( A is a_component iff ex x being Point of GX st A = Component_of x )
let A be Subset of GX; :: thesis: ( A is a_component iff ex x being Point of GX st A = Component_of x )
hereby :: thesis: ( ex x being Point of GX st A = Component_of x implies A is a_component )
assume A1: A is a_component ; :: thesis: ex x being Point of GX st A = Component_of x
then A <> {} GX ;
then consider y being Point of GX such that
A2: y in A by PRE_TOPC:12;
take x = y; :: thesis: A = Component_of x
consider F being Subset-Family of GX such that
A3: for B being Subset of GX holds
( B in F iff ( B is connected & x in B ) ) and
A4: union F = Component_of x by Def7;
A in F by A1, A2, A3;
then A c= union F by ZFMISC_1:74;
hence A = Component_of x by A1, A4; :: thesis: verum
end;
given x being Point of GX such that A5: A = Component_of x ; :: thesis: A is a_component
for B being Subset of GX st B is connected & A c= B holds
A = B by A5, Th39;
hence A is a_component by A5; :: thesis: verum