---

Step * of Lemma supplementary-angles-preserve-congruence

∀g:EuclideanPlane. ∀a,b,c,d,e,f,a',d':Point.  (abc ≅a def ⇒ a-b-a' ⇒ d-e-d' ⇒ a'bc ≅a d'ef)
BY
{ (Auto THEN ParallelOp -3 THEN ExRepD THEN (D 0 THENL [Auto; Id])) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. d' : Point
10. a ≠ b
11. b ≠ c
12. d ≠ e
13. e ≠ f
14. a1 : Point
15. c' : Point
16. x' : Point
17. z' : Point
18. b_a_a1
19. b_c_c'
20. e_d_x'
21. e_f_z'
22. ba1 ≅ ex'
23. bc' ≅ ez'
24. a1c' ≅ x'z'
25. a-b-a'
26. d-e-d'
⊢ ∃a'@0,c',x',z':Point. (b_a'_a'@0 ∧ b_c_c' ∧ e_d'_x' ∧ e_f_z' ∧ ba'@0 ≅ ex' ∧ bc' ≅ ez' ∧ a'@0c' ≅ x'z')

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  ParallelOp  -3  THEN  ExRepD  THEN  (D  0  THENL  [Auto;  Id]))

---

Home Index