Theorem: Steiner-Lehmus Theorem

Let $ABC$ be a triangle.
Denote the lengths of the angle bisectors through the vertices $A$ and $B$ by $\omega_\alpha$ and $\omega_\beta$.
Let $\omega_\alpha = \omega_\beta$.
Then $ABC$ is an isosceles triangle.
:250px

Proof:
:300px
Draw $DF \parallel BE$ and $EF \parallel BD$.
By Quadrilateral is Parallelogram iff Both Pairs of Opposite Sides are Equal or Parallel:
:$\Box BEFD$ is a parallelogram.
:$\leadsto \angle DFE = \beta$
Draw $FA$.
Let $\angle EFA = \gamma$.
Let $\angle EAF = \delta$.
{{AimForCont}} $\alpha > \beta$.
Compare $\triangle BAD$ with $\triangle ABE$.  
The base is the same, $BA$.
{{begin-eqn}}
{{eqn | l = BE
      | r = AD
      | c = {{hypothesis}}
}}
{{eqn | l = \alpha
      | o = >
      | r = \beta
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = BD
      | o = >
      | r = AE
      | c = Greater Angle of Triangle Subtended by Greater Side
}}
{{eqn | l = BD
      | r = EF
      | c = {{Defof|Parallelogram}}
}}
{{eqn | ll= \leadsto
      | l = EF
      | o = >
      | r = AE
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \delta 
      | o = >
      | r = \gamma
      | c = Greater Side of Triangle Subtends Greater Angle
}}
{{eqn | l = \alpha + \delta 
      | o = >
      | r = \beta + \gamma
      | c = Addition of Inequalities
}}
{{eqn | ll= \leadsto
      | l = AD 
      | o = >
      | r = DF
      | c = Greater Angle of Triangle Subtended by Greater Side
}}
{{eqn | l = DF
      | r = BE
      | c = {{Defof|Parallelogram}}
}}
{{eqn | ll= \leadsto
      | l = AD 
      | o = >
      | r = BE
      | c = 
}}
{{end-eqn}}
But this is a contradiction.
Hence by Proof by Contradiction it cannot be the case that $\alpha > \beta$.
{{qed|lemma}}
{{AimForCont}} $\beta > \alpha$.
Again compare $\triangle BAD$ with $\triangle ABE$.
They have the same base, $BC$.
{{begin-eqn}}
{{eqn | l = BE
      | r = AD
      | c = {{hypothesis}}
}}
{{eqn | l = \beta
      | o = >
      | r = \alpha
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = AE
      | o = >
      | r = BD
      | c = Greater Angle of Triangle Subtended by Greater Side
}}
{{eqn | l = BD
      | r = EF
      | c = {{Defof|Parallelogram}}
}}
{{eqn | ll= \leadsto
      | l = AE
      | o = >
      | r = EF
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \gamma 
      | o = >
      | r = \delta
      | c = Greater Side of Triangle Subtends Greater Angle
}}
{{eqn | l = \beta + \gamma 
      | o = >
      | r = \alpha + \delta
      | c = Addition of Inequalities
}}
{{eqn | ll= \leadsto
      | l = AD 
      | o = >
      | r = DF
      | c = Greater Angle of Triangle Subtended by Greater Side
}}
{{eqn | l = DF
      | r = BE
      | c = {{Defof|Parallelogram}}
}}
{{eqn | ll= \leadsto
      | l = AD 
      | o = >
      | r = BE
      | c = 
}}
{{end-eqn}}
But this is a contradiction.
Hence by Proof by Contradiction it cannot be the case that $\alpha > \beta$.
{{qed|lemma}}
Since neither $\alpha > \beta$ nor $\alpha < \beta$, it must be the case that
:$\alpha = \beta$
So by addition:
:$\angle ABC = \angle BAC$
and by Triangle with Two Equal Angles is Isosceles:
:$\triangle ABC$ is isosceles.
The result follows.
{{qed}}