@MISC{TREAL_1.MIZ,
  AUTHOR = {Watanabe, Toshihiko},
  TITLE = {The {B}rouwer Fixed Point Theorem for Intervals},
  NOTE = {This paper was done under the supervision of Z. Karno while the
 author was visiting the Institute of Mathematics of Warsaw
 University in Bia{\l}ystok.},
  ACKNOWLEDGEMENT = {The author wishes to express his thanks to Professors
  A.~Trybulec and Z.~Karno for their useful suggestions and 
 many valuable comments.},
  SECTION1 = {Properties of Topological Intervals},
  SECTION2 = {Continuous Mappings Between Topological Intervals},
  SECTION3 = {Connectedness of Intervals and Brouwer Fixed Point Theorem for Intervals},
  DAY = {17},
  MONTH = {August},
  YEAR = {1992},
  ADDRESS1 = {Shinshu University\\Nagano},
  SUMMARY = {The aim is to prove, using Mizar System, the following
simplest version of the Brouwer Fixed Point Theorem \cite{BROUWER:1}.
 {\em For every continuous mapping $f : {\Bbb I} \rightarrow {\Bbb I}$ of the
topological unit interval $\Bbb I$ there exists a point $x$ such that
 $f(x) = x$} (see e.g. \cite{DUG-GRAN:1}, \cite{BROWN:1}).}}

