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 )
assume A1: A = the carrier of GX ; :: thesis: A is a_union_of_components of GX
{ B where B is Subset of GX : B is_a_component_of GX } c= bool the carrier of GX

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of GX : B is_a_component_of GX } or x in bool the carrier of GX )
assume x in { B where B is Subset of GX : B is_a_component_of GX } ; :: thesis: x in bool the carrier of GX
then ex B being Subset of GX st
( x = B & B is_a_component_of GX ) ;
hence x in bool the carrier of GX ; :: thesis: verum

end;

then reconsider S = { B where B is Subset of GX : B is_a_component_of GX } as Subset-Family of GX ;
A2: the carrier of GX = union S

proof

the carrier of GX c= union S

proof

let x be set ; :: 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 ;
A3: p in Component_of p by CONNSP_1:40;
set B3 = Component_of p;
Component_of p is_a_component_of GX by CONNSP_1:43;
then Component_of p in S ;
hence x in union S by A3, TARSKI:def 4; :: thesis: verum

end;

hence the carrier of GX = union S by XBOOLE_0:def 10; :: thesis: verum

end;

for B being Subset of GX st B in S holds
B is_a_component_of GX

proof

let B be Subset of GX; :: thesis: ( B in S implies B is_a_component_of GX )
assume B in S ; :: thesis: B is_a_component_of GX
then ex B2 being Subset of GX st
( B = B2 & B2 is_a_component_of GX ) ;
hence B is_a_component_of GX ; :: thesis: verum

end;

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