let GX be non empty TopSpace; :: thesis: Component_of ({} GX) = the carrier of GX

defpred S_{1}[ 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 S_{1}[A] )
from SUBSET_1:sch 3();

A2: for A being Subset of GX holds

( A in F iff ( A is connected & {} GX c= A ) )

hence Component_of ({} GX) = the carrier of GX by A2, Def1; :: thesis: verum

defpred S

( 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 S

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 )

end;thus ( A in F implies ( A is connected & {} GX c= A ) ) :: thesis: ( A is connected & {} GX c= A implies A in F )

proof

thus
( A is connected & {} GX c= A implies A in F )
by A1; :: thesis: verum
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;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

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 ) )

then
union F = the carrier of GX
by TARSKI:def 4;( ( 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 ) )

thus x in the carrier of GX by A3; :: thesis: verum

end;( 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 )

given Y being set such that A3:
( x in Y & Y in F )
; :: thesis: x in the carrier of GX( 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;( 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

thus x in the carrier of GX by A3; :: thesis: verum

hence Component_of ({} GX) = the carrier of GX by A2, Def1; :: thesis: verum