\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_5_01.]
Pod pretpostavkom da va\v{z}i $\neg col(A, B, C)$ pokazati da va\v{z}i $A \neq B$ i $B \neq C$ i $C \neq A$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $\neg col(A, B, C)$ va\v{z}i $\neg col(B, C, A)$ (aksioma $sym_ncol1$).} 
\proofstep{0} {Postoje ta\v{c}ka $D$  i ta\v{c}ka $E$  i ta\v{c}ka $F$  i ta\v{c}ka $G$  tako da va\v{z}i $\neg cop(D, E, F, G)$ (aksioma $I8$).} 
\proofstep{0} {Va\v{z}i $A = B$ ili $A \neq B$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A = B$.} 
\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 $\neg col(A, B, C)$ i $A = B$ i $A = C$ va\v{z}i $\neg col(A, A, A)$.} 
\proofstep{12} {Na osnovu \v{c}injenice $\neg col(A, A, A)$ postoji  ravan $\alpha$  tako da va\v{z}i $A \in \alpha$ i $A \in \alpha$ i $A \in \alpha$ (aksioma $I4a$).} 
\proofstep{12} {Va\v{z}i $A = D$ ili $A \neq D$.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $A = D$.} 
\proofstep{18} {Va\v{z}i $A = E$ ili $A \neq E$.}  

\proofstep{21}  {Pretpostavimo da va\v{z}i: $A = E$.} 
\proofstep{24} {Va\v{z}i $A = F$ ili $A \neq F$.}  

\proofstep{27}  {Pretpostavimo da va\v{z}i: $A = F$.} 
\proofstep{30} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $A = B$ i $A = C$ i $A = D$ i $A = E$ i $A = F$ va\v{z}i $\neg col(A, A, A)$.} 
\proofstep{30} {Na osnovu \v{c}injenica $\neg cop(D, E, F, G)$ i $A = B$ i $A = C$ i $A = D$ i $A = E$ i $A = F$ va\v{z}i $\neg cop(A, A, A, G)$.} 
\proofstep{30} {Na osnovu \v{c}injenica $\neg col(A, A, A)$ i $A \in \alpha$ i $A \in \alpha$ i $A \in \alpha$ i $\neg cop(A, A, A, G)$ va\v{z}i $G \not \in \alpha$ (aksioma $D4a$).} 
\proofstep{30} {Va\v{z}i $A = G$ ili $A \neq G$.}  

\proofstep{33}  {Pretpostavimo da va\v{z}i: $A = G$.} 
\proofstep{36} {Na osnovu \v{c}injenica $G \not \in \alpha$ i $A = B$ i $A = C$ i $A = D$ i $A = E$ i $A = F$ i $A = G$ va\v{z}i $A \not \in \alpha$.} 
\proofstep{36} {Na osnovu \v{c}injenica $A \not \in \alpha$ i $A \in \alpha$ dobijamo kontradikciju.}  

\proofstep{33}  {Pretpostavimo da va\v{z}i: $A \neq G$.} 
\proofstep{36} {Na osnovu \v{c}injenice $A \neq G$ postoji prava $p$  tako da va\v{z}i $A \in p$ i $G \in p$ (aksioma $I1$).} 
\proofstep{36} {Na osnovu \v{c}injenica $A \in p$ i $A \in p$ i $A \in p$ va\v{z}i $col(A, A, A)$ (aksioma $D1$).} 
\proofstep{36} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $A = B$ i $A = C$ i $A = D$ i $A = E$ i $A = F$ va\v{z}i $\neg col(A, A, A)$.} 
\proofstep{36} {Na osnovu \v{c}injenica $\neg col(A, A, A)$ i $col(A, A, A)$ dobijamo kontradikciju.} 
\proofstep{30} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{27}  {Pretpostavimo da va\v{z}i: $A \neq F$.} 
\proofstep{30} {Na osnovu \v{c}injenice $A \neq F$ postoji prava $p$  tako da va\v{z}i $A \in p$ i $F \in p$ (aksioma $I1$).} 
\proofstep{30} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $A = B$ i $A = C$ i $A = D$ i $A = E$ va\v{z}i $\neg col(A, A, A)$.} 
\proofstep{30} {Na osnovu \v{c}injenica $\neg col(A, A, A)$ i $col(A, A, A)$ dobijamo kontradikciju.} 
\proofstep{24} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{21}  {Pretpostavimo da va\v{z}i: $A \neq E$.} 
\proofstep{24} {Na osnovu \v{c}injenice $A \neq E$ postoji prava $p$  tako da va\v{z}i $A \in p$ i $E \in p$ (aksioma $I1$).} 
\proofstep{24} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $A = B$ i $A = C$ i $A = D$ va\v{z}i $\neg col(A, A, A)$.} 
\proofstep{24} {Na osnovu \v{c}injenica $\neg col(A, A, A)$ i $col(A, A, A)$ dobijamo kontradikciju.} 
\proofstep{18} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{15}  {Pretpostavimo da va\v{z}i: $A \neq D$.} 
\proofstep{18} {Na osnovu \v{c}injenice $A \neq D$ postoji prava $p$  tako da va\v{z}i $A \in p$ i $D \in p$ (aksioma $I1$).} 
\proofstep{18} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $A = B$ i $A = C$ va\v{z}i $\neg col(A, A, A)$.} 
\proofstep{18} {Na osnovu \v{c}injenica $\neg col(A, A, A)$ i $col(A, A, A)$ dobijamo kontradikciju.} 
\proofstep{12} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{9}  {Pretpostavimo da va\v{z}i: $A \neq C$.} 
\proofstep{12} {Na osnovu \v{c}injenice $A \neq C$ postoji prava $p$  tako da va\v{z}i $A \in p$ i $C \in p$ (aksioma $I1$).} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg col(B, C, A)$ i $A = B$ va\v{z}i $\neg col(A, C, A)$.} 
\proofstep{12} {Na osnovu \v{c}injenica $A \neq C$ i $A \in p$ i $C \in p$ i $\neg col(A, C, A)$ va\v{z}i $A \not \in p$ (aksioma $D2a$).} 
\proofstep{12} {Na osnovu \v{c}injenica $A \not \in p$ i $A \in p$ dobijamo kontradikciju.} 
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \neq B$.} 
\proofstep{6} {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{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 $\neg col(A, B, C)$ i $A = C$ va\v{z}i $\neg col(A, B, A)$.} 
\proofstep{12} {Na osnovu \v{c}injenica $A \neq B$ i $A \in p$ i $B \in p$ i $\neg col(A, B, A)$ va\v{z}i $A \not \in p$ (aksioma $D2a$).} 
\proofstep{12} {Na osnovu \v{c}injenica $A \not \in p$ i $A \in p$ dobijamo kontradikciju.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $A \neq C$.} 
\proofstep{12} {Na osnovu \v{c}injenice $A \neq C$ va\v{z}i $C \neq A$.} 
\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 $\neg col(A, B, C)$ i $B = C$ va\v{z}i $\neg col(A, B, B)$.} 
\proofstep{18} {Na osnovu \v{c}injenica $A \neq B$ i $A \in p$ i $B \in p$ i $\neg col(A, B, B)$ va\v{z}i $B \not \in p$ (aksioma $D2a$).} 
\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} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \neq B$ i $B \neq C$ i $C \neq A$.} 
\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}
