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

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

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

\setlength{\textheight}{22cm} 
\newtheorem{axiom}{Aksioma}
\newtheorem{theorem}{Teorema}
\newcounter{proofstepnum} 

\begin{document}

\title{High school geometry theorems}
\author{Hilbert's axiomatic system.\\
Formalizovano od strane: Sana Stojanovic Djurdjevic \\
Dokaz generisan uz pomo\'{c}: ArgoGeoChecker.}
\date{30.03.2018.}
\maketitle

\begin{theorem}[th_3_01.]
Pod pretpostavkom da va\v{z}i $\alpha \neq \beta$ i $A \in \alpha$ i $A \in \beta$ pokazati da postoji ta\v{c}ka $B$ tako da va\v{z}i $A \neq B$ i $B \in \alpha$ i $B \in \beta$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenica $\alpha \neq \beta$ i $A \in \alpha$ i $A \in \beta$ postoji ta\v{c}ka $B$  tako da va\v{z}i $A \neq B$ i $B \in \alpha$ i $B \in \beta$ (aksioma $I7$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \neq B$ i $B \in \alpha$ i $B \in \beta$.} 
QED
\hrule 
\begin{theorem}[th_3_02.]
Pod pretpostavkom da va\v{z}i $\alpha \neq \beta$ i $A \in \alpha$ i $A \in \beta$ i $A \neq B$ i $B \in \alpha$ i $B \in \beta$ pokazati da postoji prava $p$ tako da va\v{z}i $A \in p$ i $B \in p$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $A \neq B$ postoji prava $p$  tako da va\v{z}i $A \in p$ i $B \in p$ (aksioma $I1$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \in p$ i $B \in p$.} 
QED
\hrule 
\begin{theorem}[th_3_03.]
Pod pretpostavkom da va\v{z}i $\alpha \neq \beta$ i $A \in \alpha$ i $A \in \beta$ i $A \neq B$ i $B \in \alpha$ i $B \in \beta$ i $A \in p$ i $B \in p$ pokazati da va\v{z}i $p \in \alpha$ i $p \in \beta$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenica $A \neq B$ i $A \in p$ i $B \in p$ i $A \in \alpha$ i $B \in \alpha$ va\v{z}i $p \in \alpha$ (aksioma $I6$).} 
\proofstep{0} {Na osnovu \v{c}injenica $A \neq B$ i $A \in p$ i $B \in p$ i $A \in \beta$ i $B \in \beta$ va\v{z}i $p \in \beta$ (aksioma $I6$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $p \in \alpha$ i $p \in \beta$.} 
QED
\hrule 

\end{document}
