let GX be TopSpace; :: thesis: for V being Subset of GX st V is connected & V <> {} holds

Component_of V is connected

let V be Subset of GX; :: thesis: ( V is connected & V <> {} implies Component_of V is connected )

assume that

A1: V is connected and

A2: V <> {} ; :: thesis: Component_of V is connected

consider F being Subset-Family of GX such that

A3: for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) and

A4: Component_of V = union F by Def1;

A5: for A being set st A in F holds

V c= A by A3;

F <> {} by A1, A3;

then V c= meet F by A5, SETFAM_1:5;

then A6: meet F <> {} GX by A2;

for A being Subset of GX st A in F holds

A is connected by A3;

hence Component_of V is connected by A4, A6, CONNSP_1:26; :: thesis: verum

Component_of V is connected

let V be Subset of GX; :: thesis: ( V is connected & V <> {} implies Component_of V is connected )

assume that

A1: V is connected and

A2: V <> {} ; :: thesis: Component_of V is connected

consider F being Subset-Family of GX such that

A3: for A being Subset of GX holds

( A in F iff ( A is connected & V c= A ) ) and

A4: Component_of V = union F by Def1;

A5: for A being set st A in F holds

V c= A by A3;

F <> {} by A1, A3;

then V c= meet F by A5, SETFAM_1:5;

then A6: meet F <> {} GX by A2;

for A being Subset of GX st A in F holds

A is connected by A3;

hence Component_of V is connected by A4, A6, CONNSP_1:26; :: thesis: verum