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 A2, ORDERS_1:6;
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 A1, A2, A3, ZFMISC_1:74;
( Y is a_component & Y c= A ) by A1, A2, A5, ZFMISC_1:74;
then Y = A by A4, CONNSP_1:def 5
.= X by A4, A6, CONNSP_1:def 5 ;
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 A3, TARSKI:def 1; :: thesis: verum
end;
then A = X by A2, ZFMISC_1:25;
hence A is a_component by A1, A3; :: thesis: verum