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