---

Step * 1 1 of Lemma vertical-angles-congruent


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'
9. A' : Point
10. b-a'-A' ∧ a'A' ≅ ab
11. A : Point
12. b-a-A ∧ aA ≅ ba'
13. C' : Point
14. b-c'-C' ∧ c'C' ≅ bc
15. C : Point
16. b-c-C ∧ cC ≅ bc'
17. AC ≅ A'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')
BY
{ (InstConcl [⌜A⌝;⌜C⌝;⌜A'⌝;⌜C'⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

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'
9.  A'  :  Point
10.  b-a'-A'  \mwedge{}  a'A'  \mcong{}  ab
11.  A  :  Point
12.  b-a-A  \mwedge{}  aA  \mcong{}  ba'
13.  C'  :  Point
14.  b-c'-C'  \mwedge{}  c'C'  \mcong{}  bc
15.  C  :  Point
16.  b-c-C  \mwedge{}  cC  \mcong{}  bc'
17.  AC  \mcong{}  A'C'
\mvdash{}  \mexists{}a'@0,c'@0,x',z':Point
      (b\_a\_a'@0  \mwedge{}  b\_c\_c'@0  \mwedge{}  b\_a'\_x'  \mwedge{}  b\_c'\_z'  \mwedge{}  ba'@0  \mcong{}  bx'  \mwedge{}  bc'@0  \mcong{}  bz'  \mwedge{}  a'@0c'@0  \mcong{}  x'z')


By

---

Latex:
(InstConcl  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}A'\mkleeneclose{};\mkleeneopen{}C'\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index