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

let A be non empty a_union_of_components of T; :: thesis: ( A is connected implies A is a_component )
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 and
A2: A = union F by Def2;
consider X being set such that
X <> {} and
A3: X in F by ;
reconsider X = X as Subset of T by A3;
assume A4: A is connected ; :: thesis: A is a_component
F = {X}
proof
thus F c= {X} :: according to XBOOLE_0:def 10 :: thesis: {X} c= F
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in {X} )
assume A5: x in F ; :: thesis: x in {X}
then reconsider Y = x as Subset of T ;
A6: ( X is a_component & X c= A ) by ;
( Y is a_component & Y c= A ) by ;
then Y = A by
.= X by ;
hence x in {X} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: 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 ; :: thesis: verum
end;
then A = X by ;
hence A is a_component by A1, A3; :: thesis: verum