let GX be non empty TopSpace; :: thesis: for x being Point of GX holds Component_of x is connected
let x be Point of GX; :: thesis: Component_of x is connected
consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) and
A2: Component_of x = union F by Def7;
A3: for A being set st A in F holds
x in A by A1;
A4: for A being Subset of GX st A in F holds
A is connected by A1;
F <> {} by A1, Th33;
then meet F <> {} GX by A3, SETFAM_1:def 1;
hence Component_of x is connected by A2, A4, Th27; :: thesis: verum