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