Perpendicular from a point to a line exists and is unique

Dependencies: Protractor axiom, Linear pair sums to 180°, SAS congruence, Exterior angle > either non-adjacent interior angle.

Statement

Let $\ell$ be a line and $P$ any point in the plane (either $P\in\ell$ or $P\notin\ell$). Then there exists and is unique a line $\ell'$ through $P$ that is perpendicular to $\ell$.