@MISC{TSEP_1.MIZ,
  AUTHOR = {Karno, Zbigniew},
  TITLE = {Separated and Weakly Separated Subspaces of Topological Spaces},
  ACKNOWLEDGEMENT = {I would like to express my gratitude to Professors
A. Trybulec and C. Byli\'nski for their valuable advice.
I am also extremely grateful to W.A. Trybulec and to all participants of the
Mizar Summer School (1991) for acquainting me with the Mizar system.},
  SECTION1 = {Some properties of subspaces of topological spaces},
  SECTION2 = {Operations on subspaces of topological spaces},
  SECTION3 = {Separated and weakly separated subsets of topological spaces},
  SECTION4 = {Separated and weakly separated subspaces of topological spaces},
  DAY = {08},
  MONTH = {January},
  YEAR = {1992},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {A new concept of weakly separated subsets
and subspaces of topological spaces is described in Mizar formalizm.
Based on \cite{KURAT:2}, in comparison with the notion of separated
subsets (subspaces), some properties of such subsets (subspaces)
are discussed. Some necessary facts concerning
closed subspaces, open subspaces and the union and the meet of two
subspaces are also introduced. To present the main theorems we first
formulate basic definitions. Let $X$ be a topological space. Two subsets
 $A_1$ and $A_2$ of $X$ are called {\em weakly separated} if
 $A_1 \setminus A_2$ and $A_2 \setminus A_1$ are separated.
Two subspaces $X_{1}$ and $X_{2}$ of $X$ are called {\em weakly separated}
if their carriers are weakly separated. The following theorem contains
a useful characterization of weakly separated subsets in the special case
when $A_{1} \cup A_{2}$ is equal to the carrier of $X$. {\em $A_{1}$ and
 $A_{2}$ are weakly separated iff there are such subsets of $X$, $C_{1}$ 
and $C_{2}$
closed (open) and $C$ open (closed, respectively), that
 $A_{1} \cup A_{2} = C_{1} \cup C_{2} \cup C$, $C_{1} \subset A_{1}$,
 $C_{2} \subset A_{2}$ and $C \subset A_{1} \cap A_{2}$}.
Next theorem divided into two parts contains similar characterization
of weakly separated subspaces in the special case when the union of
 $X_1$ and $X_2$ is equal to $X$. {\em If $X_{1}$ meets $X_{2}$, then
 $X_1$ and $X_2$ are weakly separated iff either $X_{1}$ is a subspace of
 $X_2$ or $X_2$ is a subspace of $X_{1}$ or there are such open (closed)
subspaces $Y_1$ and $Y_2$ of $X$ that $Y_1$ is a subspace of $X_1$
and $Y_2$ is a subspace of $X_2$ and either $X$ is equal to the union of
 $Y_1$ and $Y_2$ or there is a(n) closed (open, respectively) subspace
 $Y$ of $X$ being a subspace of the meet of $X_1$ and $X_2$ and with the
property that $X$ is the union of all $Y_1$, $Y_2$ and $Y$}.
{\em If $X_1$ misses $X_{2}$, then $X_1$ and $X_2$ are weakly separated
iff $X_1$ and $X_2$ are open (closed) subspaces of $X$}. Moreover, the
following simple characterization of separated subspaces by means of weakly
separated ones is obtained. {\em $X_1$ and $X_2$ are separated iff
there are weakly separated subspaces $Y_1$ and $Y_2$ of $X$ such that
 $X_1$ is a subspace of $Y_1$, $X_2$ is a subspace of $Y_2$ and
either $Y_1$ misses $Y_2$ or the meet of $Y_1$ and $Y_2$ misses
the union of $X_1$ and $X_2$}.}}


@BOOK{KURAT:2,
       AUTHOR = {Kazimierz Kuratowski},
        TITLE = {Topology},
    PUBLISHER = {PWN - Polish Scientific Publishers, Academic Press},
         YEAR = {1966},
       VOLUME = {I},
      ADDRESS = {Warsaw, New York and London}}