---

Step * of Lemma Euclid-Prop2

∀e:EuclideanPlane. ∀a,b,c:Point.  (∃x:{Point| ax ≅ bc})
BY
{ (Auto
   THEN (InstLemma `geo-sep-exists` [⌜e⌝;⌜a⌝]⋅ THENA Auto)
   THEN D -1
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜a⌝;⌜A'⌝;⌜b⌝]⋅ THENA Auto)
   THEN D -1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. A' : Point
6. a ≠ A'
7. a ≠ b
⊢ ∃x:{Point| ax ≅ bc}

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. A' : Point
6. a ≠ A'
7. A' ≠ b
⊢ ∃x:{Point| ax ≅ bc}

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.    (\mexists{}x:\{Point|  ax  \00D0  bc\})


By

---

Latex:
(Auto
  THEN  (InstLemma  `geo-sep-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}A'\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index