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

for F being Subset-Family of GX st ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) holds

F <> {}

let x be Point of GX; :: thesis: for F being Subset-Family of GX st ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) holds

F <> {}

let F be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) implies F <> {} )

assume A1: for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ; :: thesis: F <> {}

x in {x} by TARSKI:def 1;

hence F <> {} by A1; :: thesis: verum

for F being Subset-Family of GX st ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) holds

F <> {}

let x be Point of GX; :: thesis: for F being Subset-Family of GX st ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) holds

F <> {}

let F be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ) implies F <> {} )

assume A1: for A being Subset of GX holds

( A in F iff ( A is connected & x in A ) ) ; :: thesis: F <> {}

x in {x} by TARSKI:def 1;

hence F <> {} by A1; :: thesis: verum