\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_6_01.]
Pod pretpostavkom da va\v{z}i $p \neq q$ i $q \neq r$ i $r \neq p$ i $ \textrm{prave } p \textrm{ i } q \textrm{ se seku} $ i $ \textrm{prave } q \textrm{ i } r \textrm{ se seku} $ i $ \textrm{prave } r \textrm{ i } p \textrm{ se seku} $ i $A \in p$ i $A \in q$ i $A \not \in r$ i $B \not \in p$ i $B \in q$ i $B \in r$ i $C \in p$ i $C \not \in q$ i $C \in r$ pokazati da postoji ravan $\alpha$ tako da va\v{z}i $A \in \alpha$ i $B \in \alpha$ i $C \in \alpha$.
\end{theorem}

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


\proofstep{0} {Va\v{z}i $A = B$ ili $A \neq B$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A = B$.} 
\proofstep{6} {Na osnovu \v{c}injenica $B \not \in p$ i $A = B$ va\v{z}i $A \not \in p$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \not \in p$ i $A \in p$ dobijamo kontradikciju.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \neq B$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq B$ i $A \in q$ i $B \in q$ i $C \not \in q$ va\v{z}i $\neg col(A, B, C)$ (aksioma $D1a$).} 
\proofstep{6} {Na osnovu \v{c}injenice $\neg col(A, B, C)$ postoji  ravan $\alpha$  tako da va\v{z}i $A \in \alpha$ i $B \in \alpha$ i $C \in \alpha$ (aksioma $I4a$).} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \in \alpha$ i $B \in \alpha$ i $C \in \alpha$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_6_02.]
Pod pretpostavkom da va\v{z}i $p \neq q$ i $q \neq r$ i $r \neq p$ i $ \textrm{prave } p \textrm{ i } q \textrm{ se seku} $ i $ \textrm{prave } q \textrm{ i } r \textrm{ se seku} $ i $ \textrm{prave } r \textrm{ i } p \textrm{ se seku} $ i $A \in p$ i $A \in q$ i $A \not \in r$ i $B \not \in p$ i $B \in q$ i $B \in r$ i $C \in p$ i $C \not \in q$ i $C \in r$ i $A \in \alpha$ i $B \in \alpha$ i $C \in \alpha$ pokazati da va\v{z}i $p \in \alpha$ i $q \in \alpha$ i $r \in \alpha$.
\end{theorem}

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


\proofstep{0} {Va\v{z}i $A = B$ ili $A \neq B$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A = B$.} 
\proofstep{6} {Na osnovu \v{c}injenica $B \not \in p$ i $A = B$ va\v{z}i $A \not \in p$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \not \in p$ i $A \in p$ dobijamo kontradikciju.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \neq B$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq B$ i $A \in q$ i $B \in q$ i $A \in \alpha$ i $B \in \alpha$ va\v{z}i $q \in \alpha$ (aksioma $I6$).} 
\proofstep{6} {Va\v{z}i $A = C$ ili $A \neq C$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $A = C$.} 
\proofstep{12} {Na osnovu \v{c}injenica $C \not \in q$ i $A = C$ va\v{z}i $A \not \in q$.} 
\proofstep{12} {Na osnovu \v{c}injenica $A \not \in q$ i $A \in q$ dobijamo kontradikciju.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $A \neq C$.} 
\proofstep{12} {Na osnovu \v{c}injenica $A \neq C$ i $A \in p$ i $C \in p$ i $A \in \alpha$ i $C \in \alpha$ va\v{z}i $p \in \alpha$ (aksioma $I6$).} 
\proofstep{12} {Va\v{z}i $B = C$ ili $B \neq C$.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $B = C$.} 
\proofstep{18} {Na osnovu \v{c}injenica $C \in p$ i $B = C$ va\v{z}i $B \in p$.} 
\proofstep{18} {Na osnovu \v{c}injenica $B \not \in p$ i $B \in p$ dobijamo kontradikciju.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $B \neq C$.} 
\proofstep{18} {Na osnovu \v{c}injenica $B \neq C$ i $B \in r$ i $C \in r$ i $B \in \alpha$ i $C \in \alpha$ va\v{z}i $r \in \alpha$ (aksioma $I6$).} 

\proofstep{18} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $p \in \alpha$ i $q \in \alpha$ i $r \in \alpha$.} 
\proofstep{12} {Teorema je dokazana u svim slu\v{c}ajevima.}
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.}
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 

\end{document}
