\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_17_01.]
Pod pretpostavkom da va\v{z}i $bet(A, B, C)$ i $bet(C, B, D)$ i $bet(D, B, E)$ pokazati da postoji prava $p$ tako da va\v{z}i $A \in p$ i $C \in p$ i $D \in p$ i $E \in p$ i $B \in p$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(A, B, C)$ va\v{z}i $A \neq B$ i $A \neq C$ i $B \neq C$ i $col(A, B, C)$ i $bet(C, B, A)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(C, B, D)$ va\v{z}i $C \neq B$ i $C \neq D$ i $B \neq D$ i $col(C, B, D)$ i $bet(D, B, C)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(D, B, C)$ va\v{z}i $D \neq B$ i $D \neq C$ i $B \neq C$ i $col(D, B, C)$ i $bet(C, B, D)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(D, B, E)$ va\v{z}i $D \neq B$ i $D \neq E$ i $B \neq E$ i $col(D, B, E)$ i $bet(E, B, D)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(E, B, D)$ va\v{z}i $E \neq B$ i $E \neq D$ i $B \neq D$ i $col(E, B, D)$ i $bet(D, B, E)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(C, B, D)$ va\v{z}i $col(C, D, B)$ i $col(B, C, D)$ i $col(B, D, C)$ i $col(D, C, B)$ i $col(D, B, C)$ (aksioma $sym_col$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(D, B, E)$ va\v{z}i $col(D, E, B)$ i $col(B, D, E)$ i $col(B, E, D)$ i $col(E, D, B)$ i $col(E, B, D)$ (aksioma $sym_col$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(B, D, E)$ postoji prava $r$  tako da va\v{z}i $B \in r$ i $D \in r$ i $E \in r$ (aksioma $D2$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(B, C, D)$ postoji prava $q$  tako da va\v{z}i $B \in q$ i $C \in q$ i $D \in q$ (aksioma $D2$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(A, B, C)$ postoji prava $p$  tako da va\v{z}i $A \in p$ i $B \in p$ i $C \in p$ (aksioma $D2$).} 
\proofstep{0} {Va\v{z}i $A = D$ ili $A \neq D$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A = D$.} 
\proofstep{6} {Na osnovu \v{c}injenica $col(D, B, E)$ i $A = D$ va\v{z}i $col(A, B, E)$.} 
\proofstep{6} {Na osnovu \v{c}injenice $col(A, B, E)$ postoji prava $q$  tako da va\v{z}i $A \in q$ i $B \in q$ i $E \in q$ (aksioma $D2$).} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq B$ i $A \in p$ i $B \in p$ i $A \in q$ i $B \in q$ va\v{z}i $p = q$ (aksioma $I2$).} 
\proofstep{6} {Na osnovu \v{c}injenica $A \in p$ i $A = D$ va\v{z}i $D \in p$.} 
\proofstep{6} {Na osnovu \v{c}injenica $E \in q$ i $p = q$ va\v{z}i $E \in p$.} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \in p$ i $C \in p$ i $D \in p$ i $E \in p$ i $B \in p$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \neq D$.} 
\proofstep{6} {Na osnovu \v{c}injenica $B \neq C$ i $B \in p$ i $C \in p$ i $B \in q$ i $C \in q$ va\v{z}i $p = q$ (aksioma $I2$).} 
\proofstep{6} {Na osnovu \v{c}injenica $D \in q$ i $p = q$ va\v{z}i $D \in p$.} 
\proofstep{6} {Na osnovu \v{c}injenica $B \neq D$ i $B \in p$ i $D \in p$ i $B \in r$ i $D \in r$ va\v{z}i $p = r$ (aksioma $I2$).} 
\proofstep{6} {Na osnovu \v{c}injenica $D \in q$ i $p = q$ i $p = r$ va\v{z}i $D \in p$.} 
\proofstep{6} {Na osnovu \v{c}injenica $E \in r$ i $p = q$ i $p = r$ va\v{z}i $E \in p$.} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \in p$ i $C \in p$ i $D \in p$ i $E \in p$ i $B \in p$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_17_02.]
Pod pretpostavkom da va\v{z}i $bet(A, E, B)$ i $bet(B, E, C)$ i $bet(C, E, D)$ i $A \in u$ i $B \in u$ i $C \in u$ i $D \in u$ i $E \in u$ pokazati da va\v{z}i $bet(A, E, D)$.
\end{theorem}

\hrule 

\end{document}
