---

Step * 1 of Lemma geo-construction-unicity-from-first

.....antecedent..... 
1. e : BasicGeometry-
2. Q : Point
3. A : Point
4. X : Point
5. Y : Point
6. Q ≠ A
7. Q_A_Y
8. Q_A_X
9. QY ≅ QX
⊢ AY ≅ AX
BY
{ ((InstLemma `geo-inner-three-segment` [⌜e⌝;⌜X⌝;⌜A⌝;⌜Q⌝;⌜Y⌝;⌜A⌝;⌜Q⌝]⋅ THEN EAuto 1)
   THEN FLemma `geo-congruent-full-symmetry` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  BasicGeometry-
2.  Q  :  Point
3.  A  :  Point
4.  X  :  Point
5.  Y  :  Point
6.  Q  \mneq{}  A
7.  Q\_A\_Y
8.  Q\_A\_X
9.  QY  \mcong{}  QX
\mvdash{}  AY  \mcong{}  AX


By

---

Latex:
((InstLemma  `geo-inner-three-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)
  THEN  FLemma  `geo-congruent-full-symmetry`  [-1]
  THEN  Auto)

---

Home Index