---

Step * 1 of Lemma geo-construction-unicity

.....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. AY ≅ AX
⊢ QY ≅ QX
BY
{ (InstLemma `geo-three-segment` [⌜e⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜Q⌝;⌜A⌝;⌜Y⌝]⋅ THEN EAuto 1) }

---

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.  AY  \00D0  AX
\mvdash{}  QY  \00D0  QX


By

---

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

---

Home Index