let T be non empty TopSpace; :: thesis: for A being non empty a_union_of_components of T st A is connected holds
A is_a_component_of T
let A be non empty a_union_of_components of T; :: thesis: ( A is connected implies A is_a_component_of T )
consider F being Subset-Family of T such that
A1: ( ( for B being Subset of T st B in F holds
B is_a_component_of T ) & A = union F ) by Def2;
consider X being set such that
A2: ( X <> {} & X in F ) by A1, ORDERS_1:91;
reconsider X = X as Subset of T by A2;
assume A3: A is connected ; :: thesis: A is_a_component_of T
F = {X}

proof

thus F c= {X} :: according to XBOOLE_0:def 10 :: thesis: {X} c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in {X} )
assume A4: x in F ; :: thesis: x in {X}
then reconsider Y = x as Subset of T ;
A5: ( Y is_a_component_of T & X is_a_component_of T ) by A1, A2, A4;
A6: X c= A by A1, A2, ZFMISC_1:92;
Y c= A by A1, A4, ZFMISC_1:92;
then Y = A by A3, A5, CONNSP_1:def 5
.= X by A3, A5, A6, CONNSP_1:def 5 ;
hence x in {X} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {X} or x in F )
assume x in {X} ; :: thesis: x in F
hence x in F by A2, TARSKI:def 1; :: thesis: verum

end;

then A = X by A1, ZFMISC_1:31;
hence A is_a_component_of T by A1, A2; :: thesis: verum