let GX be non empty TopSpace; :: thesis: for A being Subset of GX st A = the carrier of GX holds

A is a_union_of_components of GX

let A be Subset of GX; :: thesis: ( A = the carrier of GX implies A is a_union_of_components of GX )

{ B where B is Subset of GX : B is a_component } c= bool the carrier of GX

A1: for B being Subset of GX st B in S holds

B is a_component

assume A = the carrier of GX ; :: thesis: A is a_union_of_components of GX

hence A is a_union_of_components of GX by A2, A1, Def2; :: thesis: verum

A is a_union_of_components of GX

let A be Subset of GX; :: thesis: ( A = the carrier of GX implies A is a_union_of_components of GX )

{ B where B is Subset of GX : B is a_component } c= bool the carrier of GX

proof

then reconsider S = { B where B is Subset of GX : B is a_component } as Subset-Family of GX ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of GX : B is a_component } or x in bool the carrier of GX )

assume x in { B where B is Subset of GX : B is a_component } ; :: thesis: x in bool the carrier of GX

then ex B being Subset of GX st

( x = B & B is a_component ) ;

hence x in bool the carrier of GX ; :: thesis: verum

end;assume x in { B where B is Subset of GX : B is a_component } ; :: thesis: x in bool the carrier of GX

then ex B being Subset of GX st

( x = B & B is a_component ) ;

hence x in bool the carrier of GX ; :: thesis: verum

A1: for B being Subset of GX st B in S holds

B is a_component

proof

the carrier of GX c= union S
let B be Subset of GX; :: thesis: ( B in S implies B is a_component )

assume B in S ; :: thesis: B is a_component

then ex B2 being Subset of GX st

( B = B2 & B2 is a_component ) ;

hence B is a_component ; :: thesis: verum

end;assume B in S ; :: thesis: B is a_component

then ex B2 being Subset of GX st

( B = B2 & B2 is a_component ) ;

hence B is a_component ; :: thesis: verum

proof

then A2:
the carrier of GX = union S
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of GX or x in union S )

assume x in the carrier of GX ; :: thesis: x in union S

then reconsider p = x as Point of GX ;

set B3 = Component_of p;

Component_of p is a_component by CONNSP_1:40;

then ( p in Component_of p & Component_of p in S ) by CONNSP_1:38;

hence x in union S by TARSKI:def 4; :: thesis: verum

end;assume x in the carrier of GX ; :: thesis: x in union S

then reconsider p = x as Point of GX ;

set B3 = Component_of p;

Component_of p is a_component by CONNSP_1:40;

then ( p in Component_of p & Component_of p in S ) by CONNSP_1:38;

hence x in union S by TARSKI:def 4; :: thesis: verum

assume A = the carrier of GX ; :: thesis: A is a_union_of_components of GX

hence A is a_union_of_components of GX by A2, A1, Def2; :: thesis: verum