@MISC{TEX_3.MIZ,
  AUTHOR = {Karno, Zbigniew},
  TITLE = {On Nowhere and Everywhere Dense Subspaces of Topological Spaces},
  SECTION1 = {Some Properties of Subsets of a Topological Space},
  SECTION2 = {Dense and Everywhere Dense Subspaces},
  SECTION3 = {Boundary and Nowhere Dense Subspaces},
  SECTION4 = {Dense and Boundary Subspaces of Non-discrete Spaces},
  SECTION5 = {Everywhere and Nowhere Dense Subspaces of Non-almost-discrete Spaces},
  DAY = {09},
  MONTH = {November},
  YEAR = {1993},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {Let $X$ be a topological space and let $X_{0}$ be a subspace
 of $X$ with the carrier $A$.
 $X_{0}$ is called {\em boundary}\/ ({\em dense}) in $X$ if $A$ is
 boundary (dense), i.e., ${\rm Int}\,A = \emptyset$
 ($\overline{A} =$ the carrier of $X$);
 $X_{0}$ is called {\em nowhere dense}\/ ({\em everywhere dense}) in $X$
 if $A$ is nowhere dense (everywhere dense), i.e.,
 ${\rm Int}\,\overline{A} = \emptyset$
 ($\overline{{\rm Int}\,A} =$ the carrier of $X$)
 (see \cite{TOPS_3.ABS} and comp. \cite{KURAT:2}).\par
 Our purpose is to list, using Mizar formalism, a number of properties
 of such subspaces, mostly in non-discrete (non-almost-discrete) spaces
 (comp. \cite{TOPS_3.ABS}).
 Recall that $X$ is called {\em discrete}\/ if every subset of $X$ is
 open (closed); $X$ is called {\em almost discrete}\/ if every
 open subset of $X$ is closed; equivalently, if every closed subset
 of $X$ is open (see \cite{TDLAT_3.ABS}, \cite{TEX_1.ABS} and comp.
  \cite{KURAT:2},\cite{KURAT:3}).
  We have the following characterization of non-discrete spaces:
  {\em $X$ is non-discrete iff there exists a boundary subspace in $X$}.
 Hence, {\em $X$ is non-discrete iff there exists a dense proper subspace
 in $X$}.  We have the following analogous characterization of 
 non-almost-discrete spaces: {\em $X$ is non-almost-discrete iff there exists
 a nowhere dense subspace in $X$}. Hence, {\em $X$ is non-almost-discrete
 iff there exists an everywhere dense proper subspace in $X$}.\par
 Note that some interdependencies between boundary, dense, nowhere
 and everywhere dense subspaces are also indicated. These have the
 form of observations in the text and they correspond to the existential
 and to the conditional clusters in the Mizar System. These clusters
 guarantee the existence and ensure the extension of types supported
 automatically by the Mizar System.}}

