---

Step * 1 2 1 of Lemma symmetric-point-construction1


1. e : BasicGeometry
2. a : Point
3. p : Point
4. a # p
5. x : Point
6. B(pax)
7. ax ≅ ap
⊢ pa ≅ ax
BY
{ ((Assert ap ≅ pa BY Auto) THEN FLemma `geo-congruent-transitivity` [-2;-1] THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  p  :  Point
4.  a  \#  p
5.  x  :  Point
6.  B(pax)
7.  ax  \mcong{}  ap
\mvdash{}  pa  \mcong{}  ax


By

---

Latex:
((Assert  ap  \mcong{}  pa  BY  Auto)  THEN  FLemma  `geo-congruent-transitivity`  [-2;-1]  THEN  EAuto  1)

---

Home Index