theorem
EuclidGeom.isAngBisLine_of_value_eq
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
{O : P}
[EuclidGeom.PtNe A O]
[EuclidGeom.PtNe B O]
[EuclidGeom.PtNe C O]
(h : ∠ A O C = ∠ C O B)
:
EuclidGeom.IsAngBisLine (ANG A O B) (LIN O C)