@misc{REALALG2.MIZ,
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {Formally Real Fields},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      SECTION1 = {Preliminaries},
      SECTION2 = {More on Ring Characteristic},
      SECTION3 = {Maximal Preorderings},
      SECTION4 = {Formally Real Fields},
      SECTION5 = {Order Relations and Strict Order Relations Revisited},
      SECTION6 = {Absolute Values},
      SECTION7 = {Squares and Square Roots},
      DAY = {29},
      MONTH = {November},
      YEAR = {2017},
      SUMMARY = {We extend the algebraic theory of ordered fields
                 in Mizar \cite{Mizar-State-2015,FourDecades,AlgHierarchy}:
                 We show that every preordering can be extended into an
                 ordering, i.e. that formally real and ordered fields coincide.
                 We also prove some charactarizations of formally real fields,
                 in particular the one by Artin and Schreier using sums of squares.
                 In the second part of the article we define absolute values
                 and the square root function.}}

@inproceedings{AlgHierarchy,
   author={Grabowski, Adam and Korniłowicz, Artur and Schwarzweller, Christoph},
   title={On algebraic hierarchies in mathematical repository of Mizar},
   booktitle={Proceedings of the 2016 Federated Conference on Computer Science and Information Systems,
              FedCSIS2016, Gda{\'{n}}sk, Poland, September 11--14, 2016},
   editors={Ganzha, Maria and Maciaszek, Leszek and Paprzycki, Marcin}.
   pages={363--371},
   year={2016},
   doi={10.15439/2016F520}}

@BOOK{Pre84,
      AUTHOR = {Alexander Prestel},
      TITLE = {Lectures on Formally Real Fields},
      PUBLISHER = {Springer Verlag},
      YEAR = {1984}}

@BOOK{KS89,
      AUTHOR = {Manfred Knebusch and Claus Scheiderer},
      TITLE = {Einf\"{u}hrung in die reelle Algebra},
      PUBLISHER = {Vieweg Verlag},
      YEAR = {1989}}

@BOOK{Jac64,
      AUTHOR = {Nathan Jacobson},
      TITLE = {Lecture Notes in Abstract Algebra,
               III. Theory of Fields and Galois Theory},
      PUBLISHER = {Springer Verlag},
      YEAR = {1964}}

@BOOK{Rad91,
      AUTHOR = {Knut Radbruch},
      TITLE = {Geordnete K\"{o}rper},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1991}}

