---

Step * of Lemma Euclid-Prop5_2

∀e:EuclideanPlane. ∀a,b,c,x,y:Point.  ((ISOΔ(a;b;c) ∧ a-b-x ∧ a-c-y) ⇒ xbc ≅a ycb)
BY
{ (Auto
   THEN (((InstLemma `segment-density-strict` [⌜e⌝;⌜b⌝;⌜x⌝]⋅ THENA Auto) THEN ExRepD) THEN RenameVar `x\'' (-2))
   THEN (gProperProlong ⌜a⌝⌜c⌝`y\''⌜b⌝⌜x'⌝⋅ THENA Auto)
   THEN GenRepD) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. ISOΔ(a;b;c)
8. a-b-x
9. a-c-y
10. x' : Point
11. b-x'-x
12. y' : Point
13. a-c-y'
14. cy' ≅ bx'
⊢ xbc ≅a ycb

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y:Point.    ((ISO\mDelta{}(a;b;c)  \mwedge{}  a-b-x  \mwedge{}  a-c-y)  {}\mRightarrow{}  xbc  \mcong{}\msuba{}  ycb)


By

---

Latex:
(Auto
  THEN  (((InstLemma  `segment-density-strict`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
              THEN  RenameVar  `x\mbackslash{}''  (-2)
              )
  THEN  (gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`y\mbackslash{}''\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}x'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  GenRepD)

---

Home Index