Working on the book: Lang, Serge & Murrow, Gene. "Geometry - Second Edition" (p. 49)
Theorem 1-2. If $L_1$ is perpendicular to line $K$, and $L_2$ is also perpendicular to line $K$, then $L_1$ is parallel to $L_2$.
I will assume that $L_1 \nparallel L_2$, and then use
PERP 1. Given a line $L$ and a point $P$, there is one and only one line through $P$, perpendicular to $L$.
to reach a contradiction.
$L_1 \nparallel L_2$ means $$ L_1 \neq L_2 \land \exists P(P \in L_1 \land P \in L_2) $$
Proof of Theorem 1-2:
$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $
$ \fitch{1.\,L_1 \perp K\\ 2.\,L_2 \perp K\\ 3.\,\forall u\forall P\exists!l(P \in l \land l \perp K) \qquad \text{[PERP 1]} }{ 4.\,\exists!l(P \in l \land l \perp K)\\ \fitch{5.\,L_1 \nparallel L_2}{ 6.\,L_1 \neq L_2 \land \exists P(P \in L_1 \land P \in L_2)\\ 7.\,L_1 \neq L_2\\ 8.\,\exists P(P \in L_1 \land P \in L_2)\\ \fitch{9.\,P \in L_1 \land P \in L_2}{ \fitch{10.\,P \in Z \land Z \perp K \land \forall l'(P \in l' \land l' \perp K \to l' = Z)}{ 11.\,\forall l'(P \in l' \land l' \perp K \to l' = Z)\\ 12.\,P \in L_1 \land L_1 \perp K \to L_1 = Z\\ 13.\,P \in L_2 \land L_1 \perp K \to L_2 = Z\\ 14.\,L_1 = L_2 }\\ 15.\,L_1 = L_2 }\\ 16.\,L_1 = L_2\\ 17.\,\bot }\\ 18.\,L_1 \parallel L_2 } $
Is this a good proof skeleton ? Am I heading in the right direction ?
P.D.: rules of inference can be found in Appendix C of this book: http://forallx.openlogicproject.org/forallxyyc.pdf