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

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

( A in F iff ( A is open & A is closed & x in A ) ) ) holds

F <> {}

A1: ( [#] X is open & [#] X is closed ) ;

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

( A in F iff ( A is open & A is closed & x in A ) ) ) holds

F <> {}

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

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

assume for A being Subset of X holds

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

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

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

( A in F iff ( A is open & A is closed & x in A ) ) ) holds

F <> {}

A1: ( [#] X is open & [#] X is closed ) ;

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

( A in F iff ( A is open & A is closed & x in A ) ) ) holds

F <> {}

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

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

assume for A being Subset of X holds

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

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