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}

hence A is a_component by A1, A3; :: thesis: verum

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

then
A = X
by A2, ZFMISC_1:25;
thus
F c= {X}
:: according to XBOOLE_0:def 10 :: thesis: {X} c= F

assume x in {X} ; :: thesis: x in F

hence x in F by A3, TARSKI:def 1; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {X} or x in F )
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;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

assume x in {X} ; :: thesis: x in F

hence x in F by A3, TARSKI:def 1; :: thesis: verum

hence A is a_component by A1, A3; :: thesis: verum