---

Step * of Lemma geo-congruent-between-implies-equal

∀e:BasicGeometry. ∀[a,b,c,x:Point].  (b ≡ x) supposing (a_b_c and ab ≅ ax and bc ≅ xc)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (gProveSeparatedWhenStable ⌜a⌝ ⌜b⌝⋅ THENA Auto)
   THEN (InstLemma `geo-inner-five-segment` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜b⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜x⌝]⋅ THENA Auto)
   THEN gEliminatePoints
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[a,b,c,x:Point].    (b  \mequiv{}  x)  supposing  (a\_b\_c  and  ab  \00D0  ax  and  bc  \00D0  xc)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (gProveSeparatedWhenStable  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-inner-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  gEliminatePoints
  THEN  Auto)

---

Home Index