@MISC{TDLAT_3.MIZ,
  AUTHOR = {Karno, Zbigniew},
  TITLE = {The Lattice of Domains of an Extremally Disconnected Space},
  NOTE = {{\it Editor's Note:} This work has won the 1992 \'Sleszy\'nski's Award
of the Mizar Society.},
  ACKNOWLEDGEMENT = {The author wishes to thank to Professor
  A.~Trybulec for many helpful conversations during the preparation of
  this paper. The author is also very grateful to 
  Cz.~Byli\'nski for acquainting him with new PC Mizar utilities programs.},
  SECTION1 = {Selected Properties of Subsets of a Topological Space},
  SECTION2 = {Discrete Topological Structures},
  SECTION3 = {Discrete Topological Spaces},
  SECTION4 = {Extremally Disconnected Topological Spaces},
  SECTION5 = {The Lattice of Domains of Extremally Disconnected Spaces},
  DAY = {27},
  MONTH = {August},
  YEAR = {1992},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  SUMMARY = {Let $X$ be a topological space and let $A$ be a subset of $X$.
Recall that $A$ is said to be a {\em domain}\/ in $X$ provided
 ${\rm Int}\, \overline{A} \subseteq A
    \subseteq \overline{{\rm Int}\,A}$
(see \cite{TOPS_1.ABS}, \cite{ISOMICHI}). Recall also that
 $A$ is said to be a(n) {\em closed}\/ ({\em open})\/ {\em domain}\/ in $X$ if
 $A = \overline{{\rm Int}\,A}$ ($A = {\rm Int}\,\overline{A}$, resp.)
(see e.g. \cite{KURAT:2}, \cite{TOPS_1.ABS}).
It is well-known that for a given topological space all its closed
domains form a Boolean lattice, and similarly all its open domains
form a Boolean lattice, too (see e.g., \cite{MOST-KURAT:3},
  \cite{BIRKHOFF:1}). In \cite{TDLAT_1.ABS} it is proved that all domains
of a given topological space form a complemented lattice.
One may ask whether the lattice of all domains is Boolean.
The aim is to give an answer to this question.\par
 To present the main results we first recall the definition of a class
 of topological spaces which is important here. $X$ is called
 {\em extremally disconnected}\/ if for every open subset $A$ of $X$
 the closure $\overline {A}$ is open in $X$ \cite{STONE:1}
  (comp. \cite{ENGEL:1}).
 It is shown here, using Mizar System, that {\em the lattice of all
 domains of a topological space $X$ is modular iff $X$ is extremally
 disconnected.} Moreover, for every extremally disconnected space
 the lattice of all its domains coincides with both the lattice of all
 its closed domains and the lattice of all its open domains.
 From these facts it follows that {\em the lattice of all
 domains of a topological space $X$ is Boolean iff $X$ is extremally
 disconnected.}\par
 Note that we also review some of the standard facts on discrete,
 anti-discrete, almost discrete, extremally disconnected and
 hereditarily extremally disconnected topological spaces
 (comp. \cite{KURAT:2}, \cite{ENGEL:1}).}}

