---

Step * of Lemma eu-construction-unicity

∀e:EuclideanPlane. ∀[Q,A,X,Y:Point].  (X = Y ∈ Point) supposing (AY=AX and Q_A_X and Q_A_Y and (¬(Q = A ∈ Point)))
BY
{ (Auto
   THEN (InstLemma `eu-five-segment` [⌜e⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜Y⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜X⌝]⋅
   THENM (FLemma `eu-congruence-identity` [-1] THEN Auto)
   )
   THEN Auto) }

1
.....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

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[Q,A,X,Y:Point].    (X  =  Y)  supposing  (AY=AX  and  Q\_A\_X  and  Q\_A\_Y  and  (\mneg{}(Q  =  A)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `eu-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{}]\mcdot{}
  THENM  (FLemma  `eu-congruence-identity`  [-1]  THEN  Auto)
  )
  THEN  Auto)

---

Home Index