@MISC{WAYBEL20.MIZ,
  AUTHOR = {Rudnicki, Piotr},
  TITLE = {Kernel Projections and Quotient Lattices},
  SECTION1 = {Preliminaries},
  SECTION2 = {Some Remarks on Lattice Product},
  SECTION3 = {Kernel Projections and Quotient Lattices},
  DAY = {06},
  MONTH = {July},
  YEAR = {1998},
  ADDRESS1 = {University of Alberta\\Edmonton},
  SUMMARY = {This article completes the Mizar formalization of Chapter I,
  Section 2 from \cite{CCL}.  After presenting some preliminary
  material (not all of which is later used in this article) we
  give the proof of theorem 2.7 (i), p.60.  We do not follow the
  hint from \cite{CCL} suggesting using the equations 2.3, p. 58.
  The proof is taken directly from the definition of continuous lattice.
  The goal of the last section is to prove the correspondence
  between the set of all congruences of a continuous lattice and
  the set of all kernel operators of the lattice which preserve
  directed sups (Corollary 2.13).}}

