---

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

∀e:BasicGeometry-. ∀[Q,A,X,Y:Point].  (X ≡ Y) supposing (QY ≅ QX and Q_A_X and Q_A_Y and Q ≠ A)
BY
{ (Auto
   THEN (InstLemma `geo-five-segment` [⌜e⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜Y⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜X⌝]⋅
   THENM (FLemma `geo-congruence-identity-sym` [-1] THEN Auto)
   )
   THEN Auto) }

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

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry-.  \mforall{}[Q,A,X,Y:Point].    (X  \mequiv{}  Y)  supposing  (QY  \mcong{}  QX  and  Q\_A\_X  and  Q\_A\_Y  and  Q  \mneq{}  A)


By

---

Latex:
(Auto
  THEN  (InstLemma  `geo-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  `geo-congruence-identity-sym`  [-1]  THEN  Auto)
  )
  THEN  Auto)

---

Home Index