---

Step * of Lemma interior-point-preserves-cong-angle

∀g:EuclideanPlane. ∀a,b,c,x,y,z,p,q:Point.
  (abc ≅a xyz ⇒ a_q_c ⇒ x_p_z ⇒ Cong3(abc,xyz) ⇒ Cong3(aqc,xpz) ⇒ x # yz ⇒ abq ≅a xyp)
BY
{ (Auto
   THEN (InstLemma `geo-inner-five-segment` [⌜g⌝;⌜c⌝;⌜q⌝;⌜a⌝;⌜b⌝;⌜z⌝;⌜p⌝;⌜x⌝;⌜y⌝]⋅
         THENA (Auto THEN D -3 THEN D -2 THEN Auto)
         )
   THEN D 0) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. abc ≅a xyz
11. a_q_c
12. x_p_z
13. Cong3(abc,xyz)
14. Cong3(aqc,xpz)
15. x # yz
16. qb ≅ py
⊢ ((a ≠ b ∧ b ≠ q) ∧ x ≠ y) ∧ y ≠ p

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. p : Point
9. q : Point
10. abc ≅a xyz
11. a_q_c
12. x_p_z
13. Cong3(abc,xyz)
14. Cong3(aqc,xpz)
15. x # yz
16. qb ≅ py
⊢ ∃a',c',x',z':Point. (b_a_a' ∧ b_q_c' ∧ y_x_x' ∧ y_p_z' ∧ ba' ≅ yx' ∧ bc' ≅ yz' ∧ a'c' ≅ x'z')

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,x,y,z,p,q:Point.
    (abc  \mcong{}\msuba{}  xyz  {}\mRightarrow{}  a\_q\_c  {}\mRightarrow{}  x\_p\_z  {}\mRightarrow{}  Cong3(abc,xyz)  {}\mRightarrow{}  Cong3(aqc,xpz)  {}\mRightarrow{}  x  \#  yz  {}\mRightarrow{}  abq  \mcong{}\msuba{}  xyp)


By

---

Latex:
(Auto
  THEN  (InstLemma  `geo-inner-five-segment`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  D  -3  THEN  D  -2  THEN  Auto)
              )
  THEN  D  0)

---

Home Index