Triangle incircle — existence and uniqueness

Dependencies: Three angle bisectors meet (incenter) (the three angle bisectors meet at $I$), Angle bisector ⇔ equidistant from sides (on the line $\Rightarrow$ equidistant from the two sides), Tangent test (a radius through the touch point $\wedge$ the radius $\perp$ the line $\Rightarrow$ tangent line).

Statement

Let $\triangle ABC$ be a non-degenerate triangle, and let $I$ be its incenter (given by Three angle bisectors meet (incenter)). Let

Then the circle $\odot(I,\, r)$ centered at $I$ with radius $r$ is tangent to all three sides $AB$, $BC$, $CA$. This circle is called the incircle of $\triangle ABC$, and the three contact points $D \in BC$, $E \in CA$, $F \in AB$ are exactly the feet of the perpendiculars from $I$ to the three sides.