let X be non empty TopSpace; :: thesis: for x being Point of
for F being Subset-Family of st ( for A being Subset of holds
( A in F iff ( A is open & A is closed & x in A ) ) ) holds
F <> {}
A1: ( [#] X is open & [#] X is closed ) by TOPS_1:53;
let x be Point of ; :: thesis: for F being Subset-Family of st ( for A being Subset of holds
( A in F iff ( A is open & A is closed & x in A ) ) ) holds
F <> {}
let F be Subset-Family of ; :: thesis: ( ( for A being Subset of holds
( A in F iff ( A is open & A is closed & x in A ) ) ) implies F <> {} )
assume for A being Subset of holds
( A in F iff ( A is open & A is closed & x in A ) ) ; :: thesis: F <> {}
hence F <> {} by A1; :: thesis: verum