let GZ be non empty TopSpace; :: thesis: for A, B being Subset of GZ st A is a_component & B is a_component holds
A \/ B is a_union_of_components of GZ
let A, B be Subset of GZ; :: thesis: ( A is a_component & B is a_component implies A \/ B is a_union_of_components of GZ )
{A,B} c= bool the carrier of GZ

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {A,B} or x in bool the carrier of GZ )
assume x in {A,B} ; :: thesis: x in bool the carrier of GZ
then ( x = A or x = B ) by TARSKI:def 2;
hence x in bool the carrier of GZ ; :: thesis: verum

end;

then reconsider F2 = {A,B} as Subset-Family of GZ ;
reconsider F = F2 as Subset-Family of GZ ;
assume ( A is a_component & B is a_component ) ; :: thesis: A \/ B is a_union_of_components of GZ
then A1: for B1 being Subset of GZ st B1 in F holds
B1 is a_component by TARSKI:def 2;
A \/ B = union F by ZFMISC_1:75;
hence A \/ B is a_union_of_components of GZ by A1, CONNSP_3:def 2; :: thesis: verum