---

Step * of Lemma Euclid-Prop2-lemma

No Annotations
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a # b} . ∀v:Point.  (∃x:Point [ax ≅ bv])
BY
{ (Auto
   THEN (InstLemma `Euclid-Prop1-left-ext` [⌜e⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto)
   THEN ExRepD
   THEN (InstLemma `extend-using-SC` [⌜e⌝;⌜c⌝;⌜b⌝;⌜v⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN RenameVar `y' (-3)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. v : Point
5. c : Point
6. cb ≅ ab
7. ca ≅ ba
8. ca ≅ cb
9. c leftof ab
10. y : Point
11. B(cby)
12. by ≅ bv
⊢ ∃x:Point [ax ≅ bv]

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}v:Point.    (\mexists{}x:Point  [ax  \mcong{}  bv])


By

---

Latex:
(Auto
  THEN  (InstLemma  `Euclid-Prop1-left-ext`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ExRepD
  THEN  (InstLemma  `extend-using-SC`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `y'  (-3))

---

Home Index