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} is connected & x in {x} ) by Th29, TARSKI:def 1;
hence F <> {} by A1; :: thesis: verum