---

Step * 1 of Lemma eu-construction-unicity

.....antecedent..... 
1. e : EuclideanPlane@i'
2. Q : Point
3. A : Point
4. X : Point
5. Y : Point
6. ¬(Q = A ∈ Point)
7. Q_A_Y
8. Q_A_X
9. AY=AX
⊢ QY=QX
BY
{ (InstLemma `eu-three-segment` [⌜e⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜Q⌝;⌜A⌝;⌜Y⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  EuclideanPlane@i'
2.  Q  :  Point
3.  A  :  Point
4.  X  :  Point
5.  Y  :  Point
6.  \mneg{}(Q  =  A)
7.  Q\_A\_Y
8.  Q\_A\_X
9.  AY=AX
\mvdash{}  QY=QX


By

---

Latex:
(InstLemma  `eu-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