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 <> {}
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 A1: for A being Subset of X holds
( A in F iff ( A is open & A is closed & x in A ) ) ; :: thesis: F <> {}
( [#] X is open & [#] X is closed & x in [#] X ) by TOPS_1:53;
hence F <> {} by A1; :: thesis: verum