\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_16_01.]
Pod pretpostavkom da va\v{z}i $A \neq B$ pokazati da postoji prava $p$  i ta\v{c}ka $C$ tako da va\v{z}i $A \in p$ i $B \in p$ i $C \not \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} {Postoje ta\v{c}ka $C$  i ta\v{c}ka $D$  i ta\v{c}ka $E$  tako da va\v{z}i $\neg col(C, D, E)$ (aksioma $I3b$).} 
\proofstep{0} {Va\v{z}i $C \in p$ ili $C \not \in p$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $C \in p$.} 
\proofstep{6} {Va\v{z}i $D \in p$ ili $D \not \in p$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $D \in p$.} 
\proofstep{12} {Va\v{z}i $E \in p$ ili $E \not \in p$.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $E \in p$.} 
\proofstep{18} {Na osnovu \v{c}injenica $C \in p$ i $D \in p$ i $E \in p$ va\v{z}i $col(C, D, E)$ (aksioma $D1$).} 
\proofstep{18} {Na osnovu \v{c}injenica $\neg col(C, D, E)$ i $col(C, D, E)$ dobijamo kontradikciju.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $E \not \in p$.} 

\proofstep{18} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \in p$ i $B \in p$ i $E \not \in p$.} 
\proofstep{12} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{9}  {Pretpostavimo da va\v{z}i: $D \not \in p$.} 

\proofstep{12} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \in p$ i $B \in p$ i $D \not \in p$.} 
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{3}  {Pretpostavimo da va\v{z}i: $C \not \in p$.} 

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

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


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

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

\proofstep{3}  {Pretpostavimo da va\v{z}i: $B \neq C$.} 
\proofstep{6} {Na osnovu \v{c}injenice $B \neq C$ postoji ta\v{c}ka $G$  tako da va\v{z}i $bet(B, C, G)$ (aksioma $II2$).} 

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

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(B, C, D)$ va\v{z}i $B \neq C$ i $B \neq D$ i $C \neq D$ i $col(B, C, D)$ i $bet(D, C, B)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(B, C, D)$ va\v{z}i $col(B, D, C)$ i $col(C, B, D)$ i $col(C, D, B)$ i $col(D, B, C)$ i $col(D, C, B)$ (aksioma $sym_col$).} 
\proofstep{0} {Na osnovu \v{c}injenice $A \neq B$ va\v{z}i $B \neq A$.} 
\proofstep{0} {Na osnovu \v{c}injenica $B \neq A$ i $B \in p$ i $A \in p$ i $C \not \in p$ va\v{z}i $\neg col(B, A, C)$ (aksioma $D1a$).} 
\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 $\neg col(B, A, C)$ i $A = D$ va\v{z}i $\neg col(B, D, C)$.} 
\proofstep{6} {Na osnovu \v{c}injenica $\neg col(B, D, C)$ i $col(B, D, C)$ dobijamo kontradikciju.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \neq D$.} 
\proofstep{6} {Na osnovu \v{c}injenice $A \neq D$ postoji ta\v{c}ka $G$  tako da va\v{z}i $bet(A, D, G)$ (aksioma $II2$).} 

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

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(B, C, D)$ va\v{z}i $B \neq C$ i $B \neq D$ i $C \neq D$ i $col(B, C, D)$ i $bet(D, C, B)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(B, C, D)$ va\v{z}i $col(B, D, C)$ i $col(C, B, D)$ i $col(C, D, B)$ i $col(D, B, C)$ i $col(D, C, B)$ (aksioma $sym_col$).} 
\proofstep{0} {Va\v{z}i $D \in p$ ili $D \not \in p$.}  

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

\proofstep{3}  {Pretpostavimo da va\v{z}i: $D \not \in p$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq B$ i $A \in p$ i $B \in p$ i $D \not \in p$ va\v{z}i $\neg col(A, B, D)$ (aksioma $D1a$).} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $\neg col(A, B, D)$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_16_05.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ pokazati da va\v{z}i $E \neq C$.
\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 $C \not \in p$ va\v{z}i $\neg col(A, B, C)$ (aksioma $D1a$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(A, D, E)$ va\v{z}i $A \neq D$ i $A \neq E$ i $D \neq E$ i $col(A, D, E)$ i $bet(E, D, A)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(B, C, D)$ va\v{z}i $B \neq C$ i $B \neq D$ i $C \neq D$ i $col(B, C, D)$ i $bet(D, C, B)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(D, C, B)$ va\v{z}i $D \neq C$ i $D \neq B$ i $C \neq B$ i $col(D, C, B)$ i $bet(B, C, D)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $A \neq D$ postoji prava $r$  tako da va\v{z}i $A \in r$ i $D \in r$ (aksioma $I1$).} 
\proofstep{0} {Va\v{z}i $C = E$ ili $C \neq E$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $C = E$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq E$ i $C = E$ va\v{z}i $A \neq C$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq C$ i $C = A$ i $A = C$ va\v{z}i $C \neq A$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq E$ i $C = E$ va\v{z}i $A \neq C$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq C$ i $C = A$ i $A = C$ va\v{z}i $C \neq A$.} 
\proofstep{6} {Va\v{z}i $B \in r$ ili $B \not \in r$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $B \in r$.} 
\proofstep{12} {Na osnovu \v{c}injenica $A \neq B$ i $A \in r$ i $B \in r$ i $\neg col(A, B, C)$ va\v{z}i $C \not \in r$ (aksioma $D2a$).} 
\proofstep{12} {Na osnovu \v{c}injenica $A \neq D$ i $A \in r$ i $D \in r$ i $C \not \in r$ va\v{z}i $\neg col(A, D, C)$ (aksioma $D1a$).} 
\proofstep{12} {Na osnovu \v{c}injenica $col(A, D, E)$ i $C = E$ va\v{z}i $col(A, D, C)$.} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg col(A, D, C)$ i $col(A, D, C)$ dobijamo kontradikciju.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $B \not \in r$.} 
\proofstep{12} {Va\v{z}i $C \in r$ ili $C \not \in r$.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $C \in r$.} 
\proofstep{18} {Na osnovu \v{c}injenica $D \neq E$ i $C = E$ va\v{z}i $D \neq C$.} 
\proofstep{18} {Na osnovu \v{c}injenice $D \neq C$ va\v{z}i $C \neq D$.} 
\proofstep{18} {Na osnovu \v{c}injenice $C \neq D$ va\v{z}i $D \neq C$.} 
\proofstep{18} {Na osnovu \v{c}injenica $D \neq C$ i $D \in r$ i $C \in r$ i $B \not \in r$ va\v{z}i $\neg col(D, C, B)$ (aksioma $D1a$).} 
\proofstep{18} {Na osnovu \v{c}injenica $\neg col(D, C, B)$ i $col(D, C, B)$ dobijamo kontradikciju.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $C \not \in r$.} 
\proofstep{18} {Na osnovu \v{c}injenica $col(A, D, E)$ i $C = E$ va\v{z}i $col(A, D, C)$.} 
\proofstep{18} {Na osnovu \v{c}injenica $\neg col(A, D, C)$ i $col(A, D, C)$ dobijamo kontradikciju.} 
\proofstep{12} {Teorema je dokazana u svim slu\v{c}ajevima.}
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{3}  {Pretpostavimo da va\v{z}i: $C \neq E$.} 
\proofstep{6} {Na osnovu \v{c}injenice $C \neq E$ va\v{z}i $E \neq C$.} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $E \neq C$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_16_06.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ pokazati da postoji prava $q$ tako da va\v{z}i $E \in q$ i $C \in q$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $E \neq C$ va\v{z}i $C \neq E$.} 
\proofstep{0} {Na osnovu \v{c}injenice $C \neq E$ postoji prava $u$  tako da va\v{z}i $C \in u$ i $E \in u$ (aksioma $I1$).} 
\proofstep{0} {Va\v{z}i $A = C$ ili $A \neq C$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A = C$.} 
\proofstep{6} {Na osnovu \v{c}injenica $E \neq C$ i $A = C$ va\v{z}i $E \neq A$.} 
\proofstep{6} {Na osnovu \v{c}injenica $E \neq A$ i $A = E$ i $E = A$ va\v{z}i $A \neq E$.} 
\proofstep{6} {Na osnovu \v{c}injenice $E \neq A$ va\v{z}i $A \neq E$.} 
\proofstep{6} {Na osnovu \v{c}injenice $A \neq E$ postoji prava $q$  tako da va\v{z}i $A \in q$ i $E \in q$ (aksioma $I1$).} 
\proofstep{6} {Na osnovu \v{c}injenica $A \in q$ i $A = C$ va\v{z}i $C \in q$.} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $E \in q$ i $C \in q$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \neq C$.} 
\proofstep{6} {Na osnovu \v{c}injenice $A \neq C$ postoji prava $q$  tako da va\v{z}i $A \in q$ i $C \in q$ (aksioma $I1$).} 
\proofstep{6} {Va\v{z}i $A = E$ ili $A \neq E$.}  

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

\proofstep{12} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $E \in q$ i $C \in q$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $A \neq E$.} 
\proofstep{12} {Na osnovu \v{c}injenice $A \neq E$ postoji prava $r$  tako da va\v{z}i $A \in r$ i $E \in r$ (aksioma $I1$).} 
\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 $E \neq C$ i $B = C$ va\v{z}i $E \neq B$.} 
\proofstep{18} {Na osnovu \v{c}injenica $E \neq B$ i $B = E$ i $E = B$ va\v{z}i $B \neq E$.} 
\proofstep{18} {Na osnovu \v{c}injenice $E \neq B$ va\v{z}i $B \neq E$.} 
\proofstep{18} {Na osnovu \v{c}injenice $B \neq E$ postoji prava $r$  tako da va\v{z}i $B \in r$ i $E \in r$ (aksioma $I1$).} 
\proofstep{18} {Na osnovu \v{c}injenica $B \in r$ i $B = C$ va\v{z}i $C \in r$.} 

\proofstep{18} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $E \in r$ i $C \in r$.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $B \neq C$.} 
\proofstep{18} {Na osnovu \v{c}injenice $B \neq C$ postoji prava $r$  tako da va\v{z}i $B \in r$ i $C \in r$ (aksioma $I1$).} 
\proofstep{18} {Va\v{z}i $B = E$ ili $B \neq E$.}  

\proofstep{21}  {Pretpostavimo da va\v{z}i: $B = E$.} 
\proofstep{24} {Na osnovu \v{c}injenica $B \in r$ i $B = E$ va\v{z}i $E \in r$.} 

\proofstep{24} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $E \in r$ i $C \in r$.}  

\proofstep{21}  {Pretpostavimo da va\v{z}i: $B \neq E$.} 

\proofstep{24} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $E \in u$ i $C \in u$.} 
\proofstep{18} {Teorema je dokazana u svim slu\v{c}ajevima.}
\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 
\begin{theorem}[th_16_07.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ pokazati da va\v{z}i $A \not \in q$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(A, D, E)$ va\v{z}i $A \neq D$ i $A \neq E$ i $D \neq E$ i $col(A, D, E)$ i $bet(E, D, A)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(B, C, D)$ va\v{z}i $B \neq C$ i $B \neq D$ i $C \neq D$ i $col(B, C, D)$ i $bet(D, C, B)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(A, D, E)$ va\v{z}i $col(A, E, D)$ i $col(D, A, E)$ i $col(D, E, A)$ i $col(E, A, D)$ i $col(E, D, A)$ (aksioma $sym_col$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(B, C, D)$ va\v{z}i $col(B, D, C)$ i $col(C, B, D)$ i $col(C, D, B)$ i $col(D, B, C)$ i $col(D, C, B)$ (aksioma $sym_col$).} 
\proofstep{0} {Na osnovu \v{c}injenica $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ va\v{z}i $\neg col(A, B, C)$ (aksioma $D1a$).} 
\proofstep{0} {Va\v{z}i $A \in q$ ili $A \not \in q$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \in q$.} 
\proofstep{6} {Va\v{z}i $B \in q$ ili $B \not \in q$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $B \in q$.} 
\proofstep{12} {Na osnovu \v{c}injenica $A \in q$ i $B \in q$ i $C \in q$ va\v{z}i $col(A, B, C)$ (aksioma $D1$).} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg col(A, B, C)$ i $col(A, B, C)$ dobijamo kontradikciju.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $B \not \in q$.} 
\proofstep{12} {Va\v{z}i $D \in q$ ili $D \not \in q$.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $D \in q$.} 
\proofstep{18} {Na osnovu \v{c}injenica $C \neq D$ i $C \in q$ i $D \in q$ i $B \not \in q$ va\v{z}i $\neg col(C, D, B)$ (aksioma $D1a$).} 
\proofstep{18} {Na osnovu \v{c}injenica $\neg col(C, D, B)$ i $col(C, D, B)$ dobijamo kontradikciju.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $D \not \in q$.} 
\proofstep{18} {Na osnovu \v{c}injenica $A \neq E$ i $A \in q$ i $E \in q$ i $D \not \in q$ va\v{z}i $\neg col(A, E, D)$ (aksioma $D1a$).} 
\proofstep{18} {Na osnovu \v{c}injenica $\neg col(A, E, D)$ i $col(A, E, D)$ dobijamo kontradikciju.} 
\proofstep{12} {Teorema je dokazana u svim slu\v{c}ajevima.}
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{3}  {Pretpostavimo da va\v{z}i: $A \not \in q$.} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $A \not \in q$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_16_08.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ pokazati da postoji ravan $\alpha$ tako da va\v{z}i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $\neg col(A, B, D)$ postoji  ravan $\alpha$  tako da va\v{z}i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ (aksioma $I4a$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$.} 
QED
\hrule 
\begin{theorem}[th_16_09.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ pokazati da va\v{z}i $C \in \alpha$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(B, C, D)$ va\v{z}i $B \neq C$ i $B \neq D$ i $C \neq D$ i $col(B, C, D)$ i $bet(D, C, B)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(B, C, D)$ postoji prava $s$  tako da va\v{z}i $B \in s$ i $C \in s$ i $D \in s$ (aksioma $D2$).} 
\proofstep{0} {Na osnovu \v{c}injenica $B \neq D$ i $B \in s$ i $D \in s$ i $B \in \alpha$ i $D \in \alpha$ va\v{z}i $s \in \alpha$ (aksioma $I6$).} 
\proofstep{0} {Na osnovu \v{c}injenica $s \in \alpha$ i $C \in s$ va\v{z}i $C \in \alpha$ (aksioma $D11$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $C \in \alpha$.} 
QED
\hrule 
\begin{theorem}[th_16_10.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $C \in \alpha$ pokazati da va\v{z}i $E \in \alpha$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(A, D, E)$ va\v{z}i $A \neq D$ i $A \neq E$ i $D \neq E$ i $col(A, D, E)$ i $bet(E, D, A)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(B, C, D)$ va\v{z}i $B \neq C$ i $B \neq D$ i $C \neq D$ i $col(B, C, D)$ i $bet(D, C, B)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(B, C, D)$ va\v{z}i $col(B, D, C)$ i $col(C, B, D)$ i $col(C, D, B)$ i $col(D, B, C)$ i $col(D, C, B)$ (aksioma $sym_col$).} 
\proofstep{0} {Na osnovu \v{c}injenice $A \neq D$ postoji prava $s$  tako da va\v{z}i $A \in s$ i $D \in s$ (aksioma $I1$).} 
\proofstep{0} {Na osnovu \v{c}injenica $A \neq D$ i $A \in s$ i $D \in s$ i $A \in \alpha$ i $D \in \alpha$ va\v{z}i $s \in \alpha$ (aksioma $I6$).} 
\proofstep{0} {Va\v{z}i $B \in q$ ili $B \not \in q$.}  

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

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $E \in \alpha$.}  

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

\proofstep{9}  {Pretpostavimo da va\v{z}i: $A \neq C$.} 
\proofstep{12} {Na osnovu \v{c}injenice $A \neq C$ postoji prava $r$  tako da va\v{z}i $A \in r$ i $C \in r$ (aksioma $I1$).} 
\proofstep{12} {Na osnovu \v{c}injenica $A \neq C$ i $A \in r$ i $C \in r$ i $A \in \alpha$ i $C \in \alpha$ va\v{z}i $r \in \alpha$ (aksioma $I6$).} 
\proofstep{12} {Va\v{z}i $B \in r$ ili $B \not \in r$.}  

\proofstep{15}  {Pretpostavimo da va\v{z}i: $B \in r$.} 
\proofstep{18} {Va\v{z}i $D \in r$ ili $D \not \in r$.}  

\proofstep{21}  {Pretpostavimo da va\v{z}i: $D \in r$.} 
\proofstep{24} {Va\v{z}i $E \in r$ ili $E \not \in r$.}  

\proofstep{27}  {Pretpostavimo da va\v{z}i: $E \in r$.} 
\proofstep{30} {Na osnovu \v{c}injenica $r \in \alpha$ i $E \in r$ va\v{z}i $E \in \alpha$ (aksioma $D11$).} 

\proofstep{30} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $E \in \alpha$.}  

\proofstep{27}  {Pretpostavimo da va\v{z}i: $E \not \in r$.} 
\proofstep{30} {Na osnovu \v{c}injenica $A \neq D$ i $A \in r$ i $D \in r$ i $E \not \in r$ va\v{z}i $\neg col(A, D, E)$ (aksioma $D1a$).} 
\proofstep{30} {Na osnovu \v{c}injenica $\neg col(A, D, E)$ i $col(A, D, E)$ dobijamo kontradikciju.} 
\proofstep{24} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{21}  {Pretpostavimo da va\v{z}i: $D \not \in r$.} 
\proofstep{24} {Na osnovu \v{c}injenica $B \neq C$ i $B \in r$ i $C \in r$ i $D \not \in r$ va\v{z}i $\neg col(B, C, D)$ (aksioma $D1a$).} 
\proofstep{24} {Na osnovu \v{c}injenica $\neg col(B, C, D)$ i $col(B, C, D)$ dobijamo kontradikciju.} 
\proofstep{18} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{15}  {Pretpostavimo da va\v{z}i: $B \not \in r$.} 
\proofstep{18} {Va\v{z}i $E \in s$ ili $E \not \in s$.}  

\proofstep{21}  {Pretpostavimo da va\v{z}i: $E \in s$.} 
\proofstep{24} {Na osnovu \v{c}injenica $s \in \alpha$ i $E \in s$ va\v{z}i $E \in \alpha$ (aksioma $D11$).} 

\proofstep{24} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $E \in \alpha$.}  

\proofstep{21}  {Pretpostavimo da va\v{z}i: $E \not \in s$.} 
\proofstep{24} {Na osnovu \v{c}injenica $A \neq D$ i $A \in s$ i $D \in s$ i $E \not \in s$ va\v{z}i $\neg col(A, D, E)$ (aksioma $D1a$).} 
\proofstep{24} {Na osnovu \v{c}injenica $\neg col(A, D, E)$ i $col(A, D, E)$ dobijamo kontradikciju.} 
\proofstep{18} {Teorema je dokazana u svim slu\v{c}ajevima.}
\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 
\begin{theorem}[th_16_11.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $C \in \alpha$ i $E \in \alpha$ pokazati da va\v{z}i $q \in \alpha$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $E \neq C$ va\v{z}i $C \neq E$.} 
\proofstep{0} {Na osnovu \v{c}injenica $C \neq E$ i $C \in q$ i $E \in q$ i $C \in \alpha$ i $E \in \alpha$ va\v{z}i $q \in \alpha$ (aksioma $I6$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $q \in \alpha$.} 
QED
\hrule 
\begin{theorem}[th_16_12.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $C \in \alpha$ i $E \in \alpha$ i $q \in \alpha$ pokazati da va\v{z}i $ \textrm{pash}( A,B,D,q,\alpha)$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(A, D, E)$ va\v{z}i $A \neq D$ i $A \neq E$ i $D \neq E$ i $col(A, D, E)$ i $bet(E, D, A)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(B, C, D)$ va\v{z}i $B \neq C$ i $B \neq D$ i $C \neq D$ i $col(B, C, D)$ i $bet(D, C, B)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(D, C, B)$ va\v{z}i $D \neq C$ i $D \neq B$ i $C \neq B$ i $col(D, C, B)$ i $bet(B, C, D)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $bet(E, D, A)$ va\v{z}i $E \neq D$ i $E \neq A$ i $D \neq A$ i $col(E, D, A)$ i $bet(A, D, E)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $D \neq E$ va\v{z}i $E \neq D$.} 
\proofstep{0} {Na osnovu \v{c}injenice $C \neq D$ va\v{z}i $D \neq C$.} 
\proofstep{0} {Va\v{z}i $B \in q$ ili $B \not \in q$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $B \in q$.} 
\proofstep{6} {Va\v{z}i $D \in q$ ili $D \not \in q$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $D \in q$.} 
\proofstep{12} {Na osnovu \v{c}injenica $E \neq D$ i $E \in q$ i $D \in q$ i $A \not \in q$ va\v{z}i $\neg col(E, D, A)$ (aksioma $D1a$).} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg col(E, D, A)$ i $col(E, D, A)$ dobijamo kontradikciju.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $D \not \in q$.} 
\proofstep{12} {Na osnovu \v{c}injenica $B \neq C$ i $B \in q$ i $C \in q$ i $D \not \in q$ va\v{z}i $\neg col(B, C, D)$ (aksioma $D1a$).} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg col(B, C, D)$ i $col(B, C, D)$ dobijamo kontradikciju.} 
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{3}  {Pretpostavimo da va\v{z}i: $B \not \in q$.} 
\proofstep{6} {Va\v{z}i $D \in q$ ili $D \not \in q$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $D \in q$.} 
\proofstep{12} {Na osnovu \v{c}injenica $D \neq C$ i $D \in q$ i $C \in q$ i $B \not \in q$ va\v{z}i $\neg col(D, C, B)$ (aksioma $D1a$).} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg col(D, C, B)$ i $col(D, C, B)$ dobijamo kontradikciju.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $D \not \in q$.} 
\proofstep{12} {Na osnovu \v{c}injenica $B \not \in q$ i $D \not \in q$ i $C \in q$ i $bet(B, C, D)$ va\v{z}i $ \textrm{prava } q \textrm{ se\v{c}e segment }BD$ (aksioma $cut_1$).} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg col(A, B, D)$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $q \in \alpha$ i $A \not \in q$ i $B \not \in q$ i $D \not \in q$ i $ \textrm{prava } q \textrm{ se\v{c}e segment }BD$ va\v{z}i $ \textrm{pash}( A,B,D,q,\alpha)$ (aksioma $pash_1$).} 

\proofstep{12} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $ \textrm{pash}( A,B,D,q,\alpha)$.} 
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.}
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_16_13.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $C \in \alpha$ i $E \in \alpha$ i $q \in \alpha$ i $ \textrm{pash}( A,B,D,q,\alpha)$ pokazati da va\v{z}i $D \neq A$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(A, D, E)$ va\v{z}i $A \neq D$ i $A \neq E$ i $D \neq E$ i $col(A, D, E)$ i $bet(E, D, A)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $A \neq D$ va\v{z}i $D \neq A$.} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $D \neq A$.} 
QED
\hrule 
\begin{theorem}[th_16_14.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $C \in \alpha$ i $E \in \alpha$ i $q \in \alpha$ i $ \textrm{pash}( A,B,D,q,\alpha)$ i $D \neq A$ pokazati da postoji prava $r$ tako da va\v{z}i $D \in r$ i $A \in r$.
\end{theorem}

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


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

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenica $D \in r$ i $A \in r$.} 
QED
\hrule 
\begin{theorem}[th_16_15.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $C \in \alpha$ i $E \in \alpha$ i $q \in \alpha$ i $ \textrm{pash}( A,B,D,q,\alpha)$ i $D \neq A$ i $D \in r$ i $A \in r$ pokazati da va\v{z}i $r \neq q$.
\end{theorem}

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


\proofstep{0} {Va\v{z}i $p = q$ ili $p \neq q$.}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $p = q$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \not \in q$ i $p = q$ 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: $p \neq q$.} 
\proofstep{6} {Va\v{z}i $q = r$ ili $q \neq r$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $q = r$.} 
\proofstep{12} {Na osnovu \v{c}injenica $A \in r$ i $q = r$ va\v{z}i $A \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: $q \neq r$.} 
\proofstep{12} {Na osnovu \v{c}injenice $q \neq r$ va\v{z}i $r \neq q$.} 

\proofstep{12} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $r \neq q$.} 
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.}
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_16_16.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $C \in \alpha$ i $E \in \alpha$ i $q \in \alpha$ i $ \textrm{pash}( A,B,D,q,\alpha)$ i $D \neq A$ i $D \in r$ i $A \in r$ i $r \neq q$ pokazati da va\v{z}i $ \textrm{prava } q \textrm{ se\v{c}e segment }AB$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $bet(A, D, E)$ va\v{z}i $A \neq D$ i $A \neq E$ i $D \neq E$ i $col(A, D, E)$ i $bet(E, D, A)$ (aksioma $II1$).} 
\proofstep{0} {Na osnovu \v{c}injenice $col(A, D, E)$ postoji prava $s$  tako da va\v{z}i $A \in s$ i $D \in s$ i $E \in s$ (aksioma $D2$).} 
\proofstep{0} {Na osnovu \v{c}injenice $r \neq q$ va\v{z}i $q \neq r$.} 
\proofstep{0} {Na osnovu \v{c}injenice $ \textrm{pash}( A,B,D,q,\alpha)$ va\v{z}i $ \textrm{prava } q \textrm{ se\v{c}e segment }DA$ ili $ \textrm{prava } q \textrm{ se\v{c}e segment }AB$ (aksioma $II4$).}  

\proofstep{3}  {Pretpostavimo da va\v{z}i: $ \textrm{prava } q \textrm{ se\v{c}e segment }DA$.} 
\proofstep{6} {Na osnovu \v{c}injenice $ \textrm{prava } q \textrm{ se\v{c}e segment }DA$ postoji ta\v{c}ka $F$  tako da va\v{z}i $D \not \in q$ i $A \not \in q$ i $F \in q$ i $bet(D, F, A)$ (aksioma $cut_2$).} 
\proofstep{6} {Na osnovu \v{c}injenice $bet(D, F, A)$ va\v{z}i $D \neq F$ i $D \neq A$ i $F \neq A$ i $col(D, F, A)$ i $bet(A, F, D)$ (aksioma $II1$).} 
\proofstep{6} {Na osnovu \v{c}injenica $D \neq F$ i $D \neq A$ i $F \neq A$ i $bet(D, F, A)$ va\v{z}i $\neg bet(F, A, D)$ i $\neg bet(A, D, F)$ (aksioma $II3$).} 
\proofstep{6} {Na osnovu \v{c}injenice $col(D, F, A)$ va\v{z}i $col(D, A, F)$ i $col(F, D, A)$ i $col(F, A, D)$ i $col(A, D, F)$ i $col(A, F, D)$ (aksioma $sym_col$).} 
\proofstep{6} {Na osnovu \v{c}injenice $D \neq A$ va\v{z}i $A \neq D$.} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq D$ i $A \in r$ i $D \in r$ i $A \in s$ i $D \in s$ va\v{z}i $r = s$ (aksioma $I2$).} 
\proofstep{6} {Na osnovu \v{c}injenice $col(A, D, F)$ postoji prava $u$  tako da va\v{z}i $A \in u$ i $D \in u$ i $F \in u$ (aksioma $D2$).} 
\proofstep{6} {Na osnovu \v{c}injenica $A \neq D$ i $A \in r$ i $D \in r$ i $A \in u$ i $D \in u$ va\v{z}i $r = u$ (aksioma $I2$).} 
\proofstep{6} {Va\v{z}i $E = F$ ili $E \neq F$.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $E = F$.} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg bet(A, D, F)$ i $E = F$ va\v{z}i $\neg bet(A, D, E)$.} 
\proofstep{12} {Na osnovu \v{c}injenica $\neg bet(A, D, E)$ i $bet(A, D, E)$ dobijamo kontradikciju.}  

\proofstep{9}  {Pretpostavimo da va\v{z}i: $E \neq F$.} 
\proofstep{12} {Na osnovu \v{c}injenica $E \in s$ i $r = s$ i $r = u$ va\v{z}i $E \in r$.} 
\proofstep{12} {Na osnovu \v{c}injenica $F \in u$ i $r = s$ i $r = u$ va\v{z}i $F \in r$.} 
\proofstep{12} {Na osnovu \v{c}injenica $E \neq F$ i $E \in q$ i $F \in q$ i $E \in r$ i $F \in r$ va\v{z}i $q = r$ (aksioma $I2$).} 
\proofstep{12} {Na osnovu \v{c}injenica $q \neq r$ i $q = r$ dobijamo kontradikciju.} 
\proofstep{6} {Teorema je dokazana u svim slu\v{c}ajevima.} 

\proofstep{3}  {Pretpostavimo da va\v{z}i: $ \textrm{prava } q \textrm{ se\v{c}e segment }AB$.} 

\proofstep{6} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $ \textrm{prava } q \textrm{ se\v{c}e segment }AB$.} 
\proofstep{0} {Teorema je dokazana u svim slu\v{c}ajevima.}
QED
\hrule 
\begin{theorem}[th_16_17.]
Pod pretpostavkom da va\v{z}i $A \neq B$ i $A \in p$ i $B \in p$ i $C \not \in p$ i $bet(B, C, D)$ i $bet(A, D, E)$ i $\neg col(A, B, D)$ i $E \neq C$ i $E \in q$ i $C \in q$ i $A \not \in q$ i $A \in \alpha$ i $B \in \alpha$ i $D \in \alpha$ i $C \in \alpha$ i $E \in \alpha$ i $q \in \alpha$ i $ \textrm{pash}( A,B,D,q,\alpha)$ i $D \neq A$ i $D \in r$ i $A \in r$ i $r \neq q$ i $ \textrm{prava } q \textrm{ se\v{c}e segment }AB$ pokazati da postoji ta\v{c}ka $F$ tako da va\v{z}i $bet(A, F, B)$.
\end{theorem}

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


\proofstep{0} {Na osnovu \v{c}injenice $ \textrm{prava } q \textrm{ se\v{c}e segment }AB$ postoji ta\v{c}ka $F$  tako da va\v{z}i $A \not \in q$ i $B \not \in q$ i $F \in q$ i $bet(A, F, B)$ (aksioma $cut_2$).} 

\proofstep{0} {Zaklju\v{c}ak teoreme sledi iz \v{c}injenice $bet(A, F, B)$.} 
QED
\hrule 

\end{document}
