---

Step * of Lemma geo-cong-angle-transitivity

No Annotations
∀e:BasicGeometry. ∀a,b,c,x,y,z,p,q,r:Point.  (abc ≅a xyz ⇒ xyz ≅a pqr ⇒ abc ≅a pqr)
BY
{ (Auto
   THEN (Assert (a # b ∧ c # b) ∧ x # y ∧ z # y BY
               (D -2 THEN Auto))
   THEN (Assert p # q ∧ r # q BY
               (D -2 THEN Auto))
   THEN RepeatFor 2 (PromoteHyp (-1) (-4))
   THEN ExRepD) }

1
1. e : BasicGeometry
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. r : Point
11. a # b
12. c # b
13. x # y
14. z # y
15. p # q
16. r # q
17. abc ≅a xyz
18. xyz ≅a pqr
⊢ abc ≅a pqr

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,y,z,p,q,r:Point.    (abc  \mcong{}\msuba{}  xyz  {}\mRightarrow{}  xyz  \mcong{}\msuba{}  pqr  {}\mRightarrow{}  abc  \mcong{}\msuba{}  pqr)


By

---

Latex:
(Auto
  THEN  (Assert  (a  \#  b  \mwedge{}  c  \#  b)  \mwedge{}  x  \#  y  \mwedge{}  z  \#  y  BY
                          (D  -2  THEN  Auto))
  THEN  (Assert  p  \#  q  \mwedge{}  r  \#  q  BY
                          (D  -2  THEN  Auto))
  THEN  RepeatFor  2  (PromoteHyp  (-1)  (-4))
  THEN  ExRepD)

---

Home Index