let GX be non empty TopSpace; :: thesis: Component_of ({} GX) = the carrier of GX
defpred S1[ set ] means ex A1 being Subset of GX st
( A1 = \$1 & A1 is connected & {} GX c= \$1 );
consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds
( A in F iff S1[A] ) from A2: for A being Subset of GX holds
( A in F iff ( A is connected & {} GX c= A ) )
proof
let A be Subset of GX; :: thesis: ( A in F iff ( A is connected & {} GX c= A ) )
thus ( A in F implies ( A is connected & {} GX c= A ) ) :: thesis: ( A is connected & {} GX c= A implies A in F )
proof
assume A in F ; :: thesis: ( A is connected & {} GX c= A )
then ex A1 being Subset of GX st
( A1 = A & A1 is connected & {} GX c= A ) by A1;
hence ( A is connected & {} GX c= A ) ; :: thesis: verum
end;
thus ( A is connected & {} GX c= A implies A in F ) by A1; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in the carrier of GX implies ex Y being set st
( x in Y & Y in F ) ) & ( ex Y being set st
( x in Y & Y in F ) implies x in the carrier of GX ) )
let x be object ; :: thesis: ( ( x in the carrier of GX implies ex Y being set st
( x in Y & Y in F ) ) & ( ex Y being set st
( x in Y & Y in F ) implies x in the carrier of GX ) )

hereby :: thesis: ( ex Y being set st
( x in Y & Y in F ) implies x in the carrier of GX )
assume x in the carrier of GX ; :: thesis: ex Y being set st
( x in Y & Y in F )

then reconsider p = x as Point of GX ;
reconsider Y = Component_of p as set ;
take Y = Y; :: thesis: ( x in Y & Y in F )
thus x in Y by CONNSP_1:38; :: thesis: Y in F
( Component_of p is connected & {} GX c= Y ) ;
hence Y in F by A2; :: thesis: verum
end;
given Y being set such that A3: ( x in Y & Y in F ) ; :: thesis: x in the carrier of GX
thus x in the carrier of GX by A3; :: thesis: verum
end;
then union F = the carrier of GX by TARSKI:def 4;
hence Component_of ({} GX) = the carrier of GX by ; :: thesis: verum