\documentclass{article}
\usepackage{argoclp}
\catcode`\_=\active
\def_{\_}

\def\d{{\fontencoding{T1}\selectfont\dj}}

\def\D{{\fontencoding{T1}\selectfont\DJ}}

\setlength{\textheight}{22cm} 
\newtheorem{axiom}{Axiom}
\newtheorem{theorem}{Theorem}
\newcounter{proofstepnum} 

\begin{document}

\title{High school geometry theorems}
\author{Hilbert's axiomatic system.\\
Formalized by: Sana Stojanovic Djurdjevic \\
Proved by: ArgoGeoChecker.}
\date{30.03.2018.}
\maketitle

\begin{theorem}[th_1_01.]
Assuming that $A \not \in p$ there exist point $B$, point $C$, such that $B \neq C$ and $B \in p$ and $C \in p$.
\end{theorem}

{\em Proof:}
\setcounter{proofstepnum}{0} 


\proofstep{0} {There exist a point $B$ and a point $C$ where $B \neq C$ and $B \in p$ and $C \in p$ (using $ax_I3a$).} 

\proofstep{0} {The conclusion follows from the facts $B \neq C$ and $B \in p$ and $C \in p$.} 
QED
\hrule 

\end{document}
