@ARTICLE{GTARSKI5.MIZ,
    TITLE = {Tarski Geometry Axioms. {P}art {V} -- Half-planes and Planes},
    AUTHOR = {Coghetto, Roland and Grabowski, Adam},
    ADDRESS1 = {cafr-MSA2P asbl\\Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
      ADDRESS2 = {Faculty of Computer Science\\University of Bia{\l}ystok\\Poland},
      SUMMARY = {In the article, we continue \cite{GTARSKI3.ABS,GTARSKI4.ABS} the formalization of the work devoted to Tarski's geometry -- the book ``Metamathematische Methoden in der Geometrie" (SST for short) by W. Schwabh\"auser, W. Szmielew, and A. Tarski \cite{Schwabhauser:1983}, \cite{Grabowski:FedCSIS2016}, \cite{GrabowskiCoghetto:2016}. 
We use the Mizar system(\cite{Mizar-State-2015}, \cite{BancerekJAR:2018}) to formalize Chapter~9 of the SST book.\par 
We define the notion of half-plane and plane and prove some of its basic properties, 
a theory of intersecting lines (including orthogonality).} 
    MSC2010 = {51A05 51M04 68T99 03B35},
    KEYWORDS = {Tarski geometry; foundations of geometry; planes; half-plane }}

