theorem EuclidGeom.Exercise_XT_8_1_11.c_ne_B {P : Type u_1} {B : P} {C : P} : C ≠ B

theorem EuclidGeom.Exercise_XT_8_1_11.B_ne_a {P : Type u_1} {A : P} {B : P} : B ≠ A

theorem EuclidGeom.Exercise_XT_8_1_11.A_ne_C {P : Type u_1} {A : P} {C : P} : A ≠ C

theorem EuclidGeom.Exercise_XT_8_1_11.c_ne_x1 {P : Type u_1} {C : P} {X₁ : P} : C ≠ X₁

theorem EuclidGeom.Exercise_XT_8_1_11.B_ne_x2 {P : Type u_1} {B : P} {X₂ : P} : B ≠ X₂

theorem EuclidGeom.Exercise_XT_8_1_11.A_ne_y1 {P : Type u_1} {A : P} {Y₁ : P} : A ≠ Y₁

theorem EuclidGeom.Exercise_XT_8_1_11.c_ne_y2 {P : Type u_1} {C : P} {Y₂ : P} : C ≠ Y₂

theorem EuclidGeom.Exercise_XT_8_1_11.B_ne_z1 {P : Type u_1} {B : P} {Z₁ : P} : B ≠ Z₁

theorem EuclidGeom.Exercise_XT_8_1_11.A_ne_z2 {P : Type u_1} {A : P} {Z₂ : P} : A ≠ Z₂

theorem EuclidGeom.Exercise_XT_8_1_11.x1_ne_y2 {P : Type u_1} {X₁ : P} {Y₂ : P} : X₁ ≠ Y₂

theorem EuclidGeom.Exercise_XT_8_1_11.y1_ne_z2 {P : Type u_1} {Y₁ : P} {Z₂ : P} : Y₁ ≠ Z₂

theorem EuclidGeom.Exercise_XT_8_1_11.z1_ne_x2 {P : Type u_1} {Z₁ : P} {X₂ : P} : Z₁ ≠ X₂

theorem EuclidGeom.Exercise_XT_8_1_11.XT_8_1_11 {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {X₁ : P} {Y₁ : P} {Z₁ : P} {X₂ : P} {Y₂ : P} {Z₂ : P} : ∠ A Y₁ Z₂ (_ : A ≠ Y₁) (_ : Z₂ ≠ Y₁) + ∠ B Z₁ X₂ (_ : B ≠ Z₁) (_ : X₂ ≠ Z₁) + ∠ C X₁ Y₂ (_ : C ≠ X₁) (_ : Y₂ ≠ X₁) + ∠ Y₁ Z₂ A (_ : Y₁ ≠ Z₂) (_ : A ≠ Z₂) + ∠ Z₁ X₂ B (_ : Z₁ ≠ X₂) (_ : B ≠ X₂) + ∠ X₁ Y₂ C (_ : X₁ ≠ Y₂) (_ : C ≠ Y₂) = ∠[2 * Real.pi]