@MISC{MEASURE7.MIZ,
  AUTHOR = {Bia{\l}as, J\'ozef},
  TITLE = {The One-Dimensional {L}ebesgue Measure },
  DAY = {04},
  MONTH = {February},
  YEAR = {1995},
  ADDRESS1 = {{\L}\'od\'z University
{\L}\'od\'z},
  SUMMARY = {The paper is the crowning  of a series of articles
 written in  the  Mizar  language, being a formalization of
 notions needed  for the description of the one-dimensional
 Lebesgue measure. The formalization of the notion as classical
 as the Lebesgue measure determines the powers of the
 PC Mizar system as a tool for the strict, precise notation
 and verification of the correctness of deductive theories.
 Following the successive articles \cite{SUPINF_1.ABS},
 \cite{SUPINF_2.ABS}, \cite{MEASURE1.ABS}, \cite{MEASURE6.ABS}
 constructed so that the final one should
 include the definition and the basic properties of the Lebesgue
  measure, we observe  one  of  the paths relatively
 simple in the sense of the definition, enabling  us the
 formal  introduction  of  this  notion. This way, although
 toilsome, since  such is the nature of formal theories, is
 greatly instructive. It brings home  the proper succession
 of the introduction of the definitions of intermediate notions
 and points out to those elements of the theory which
 determine  the  essence  of  the  complexity of the notion
 being introduced.\par
    The paper includes the definition of the $\sigma$-field of
 Lebesgue  measurable sets, the definition  of the Lebesgue
 measure and the basic set  of  the theorems describing its
 properties.}}

