@MISC{LATTICEA.MIZ,
  AUTHOR = {Grabowski, Adam},
  TITLE = {Prime Filters and Ideals in Distributive Lattices},
  SECTION1 = {Preliminaries},
  SECTION2 = {Examples of Filters in Nontrivial Boolean Lattices},
  SECTION3 = {On Prime and Maximal Filters and Ideals},
  SECTION4 = {Prime Ideal Theorem for Distributive Lattices},
  SECTION5 = {The Stone Representation},
  SECTION6 = {Pseudocomplements in Lattices},
  SECTION7 = {Nachbin's Theorem for Bounded Distributive Lattices},
  DAY = {7},
  MONTH = {October},
  YEAR = {2013},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Akademicka 2, 15-267 Bia{\l}ystok\\Poland},
  SUMMARY = {The article continues the formalization
  of the lattice theory (as structures with two binary operations,
  not in terms of ordering relations).
  In the Mizar Mathematical Library, there are some attempts
  to formalize prime ideals and filters; one series of articles
  written as decoding \cite{CCL} proven some results; we tried
  however to follow
  \cite{LOPCLSET.ABS}, \cite{OPENLATT.ABS}, and \cite{LATTICE4.ABS}.
  All three were devoted to the Stone representation theorem
   \cite{StoneRepr}
  for Boolean or Heyting lattices. The main aim of the present article was
  to bridge this gap between general distributive lattices and
  Boolean algebras, having in mind that the more general approach
  will eventually replace the common proof of aforementioned
  articles.\footnote{As one of the anonymous referees pointed out,
  it would be interesting to show counterexamples showing that
  the assumptions of the distributivity and boundedness are
  necessary, and this will be our plan for future work as basic
  examples of nondistributive lattices are available as of now only
  as relational structures.}
  \par
  Because in Boolean algebras the notions of ultrafilters, prime filters
  and maximal filters coincide, we decided
  to construct some concrete examples of ultrafilters
  in nontrivial Boolean lattice. We proved also the Prime Ideal Theorem
  not as BPI (Boolean Prime Ideal), but in the more general setting.\par
  In the final section we present Nachbin theorems \cite{Nachbin},
  expressed both in terms of maximal and prime
  filters and as the unorderded spectra of a lattice
  \cite{NewGratzer}, \cite{Gratzer}. This shows that
  if the notion of maximal and prime filters coincide
  in the lattice, it is Boolean.}}

@MISC{Nachbin,
 AUTHOR={Nachbin, Leopoldo},
 TITLE={Une propri\'et\'e characteristique des algebres booleiennes},
 JOURNAL={Portugaliae Mathematica},
 YEAR=1947,
 VOLUME=6,
 PAGES={115--118}}

@MISC{StoneRepr,
 AUTHOR={Stone, Marshall H.},
 TITLE={The Theory of Representations of Boolean Algebras},
 JOURNAL={Transactions of the American Mathematical Society},
 YEAR=1936,
 VOLUME=40,
 PAGES={37--111}}

@BOOK{NewGratzer,
 AUTHOR={Gr\"atzer, George},
 TITLE={Lattice Theory: Foundation},
 YEAR=2011,
 PUBLISHER = {Birkh\"auser}}

