---

Step * of Lemma geo-construction-unicity2

∀e:EuclideanPlane. ∀[Q,A,X,Y:Point].  (X ≡ Y) supposing (AY ≅ AX 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
         )
   THEN InstLemma `geo-three-segment` [⌜e⌝;⌜Q⌝;⌜A⌝;⌜X⌝;⌜Q⌝;⌜A⌝;⌜Y⌝]⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[Q,A,X,Y:Point].    (X  \mequiv{}  Y)  supposing  (AY  \mcong{}  AX  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
              )
  THEN  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