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
proof
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;
then reconsider S = { B where B is Subset of GX : B is a_component } as Subset-Family of GX ;
A1: for B being Subset of GX st B in S holds
B is a_component
proof
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;
the carrier of GX c= union S
proof
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;
then A2: the carrier of GX = union S ;
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