let GX be non empty TopSpace; :: thesis: for x being Point of GX holds x in Component_of x

let x be Point of GX; :: thesis: x in Component_of x

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;

F <> {} by A1, Th31;

then A4: x in meet F by A3, SETFAM_1:def 1;

meet F c= union F by SETFAM_1:2;

hence x in Component_of x by A2, A4; :: thesis: verum

let x be Point of GX; :: thesis: x in Component_of x

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;

F <> {} by A1, Th31;

then A4: x in meet F by A3, SETFAM_1:def 1;

meet F c= union F by SETFAM_1:2;

hence x in Component_of x by A2, A4; :: thesis: verum