Maximal anti-discrete subspaces of topological spaces

Summary. Let X be a topological space and let A be a subset of X. A is said to be anti-discrete provided for every open subset G of X either A ∩ G = /0 or A ⊆ G; equivalently, for every closed subset F of X either A ∩ F = /0 or A ⊆ F. An anti-discrete subset M of X is said to be maximal anti-discrete provided for every anti-discrete subset A of X if M ⊆ A then M = A. A subspace of X is maximal anti-discrete iff its carrier is maximal anti-discrete in X. The purpose is to list a few properties of maximal anti-discrete sets and subspaces in Mizar formalism. It is shown that every x ∈ X is contained in a unique maximal anti-discrete subset M(x) of X, denoted in the text by MaxADSet(x). Such subset can be defined by M(x) = � {S ⊆ X: x ∈ S, and S is open or closed in X}. It has the following remarkable properties: (1) y ∈ M(x) iff M(y) = M(x), (2) either M(x)