---

Step * of Lemma vertical-angles-congruent

∀e:EuclideanPlane. ∀a,b,c,a',c':Point.  (a-b-a' ⇒ c-b-c' ⇒ abc ≅a a'bc')
BY
{ (Auto THEN (D 0 THENL [Auto; Id])) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. a-b-a'
8. c-b-c'
⊢ ∃a'@0,c'@0,x',z':Point. (b_a_a'@0 ∧ b_c_c'@0 ∧ b_a'_x' ∧ b_c'_z' ∧ ba'@0 ≅ bx' ∧ bc'@0 ≅ bz' ∧ a'@0c'@0 ≅ x'z')

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,a',c':Point.    (a-b-a'  {}\mRightarrow{}  c-b-c'  {}\mRightarrow{}  abc  \mcong{}\msuba{}  a'bc')


By

---

Latex:
(Auto  THEN  (D  0  THENL  [Auto;  Id]))

---

Home Index