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

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

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

then reconsider F2 = {A,B} as Subset-Family of GZ ;
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;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

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