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