@MISC{WAYBEL22.MIZ,
  AUTHOR = {Rudnicki, Piotr},
  TITLE = {Representation Theorem for Free Continuous Lattices},
  SECTION1 = {Preliminaries},
  SECTION2 = {Free Generators of Continuous Lattices},
  SECTION3 = {Representation Theorem for Free Continuous Lattices},
  DAY = {21},
  MONTH = {July},
  YEAR = {1998},
  ADDRESS1 = {University of Alberta\\Edmonton},
  SUMMARY = {We present the Mizar formalization of theorem 4.17,
  Chapter I from \cite{CCL}: a free continuous
  lattice with $m$ generators is isomorphic to the lattice of
  filters of $2^X$ ($\overline{\overline{X}} = m$) which is freely
  generated by $\{\uparrow x : x \in X\}$ (the set of ultrafilters).}}

