---

Step * of Lemma Euclid-Prop9-with-between

∀e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| c # ba} .  ∃f:Point. (acf ≅a bcf ∧ a-f-b)
BY
{ ((Auto THEN (Assert c # ba BY (DVar `c' THEN Unhide THEN Auto)) THEN D -2 THEN Thin (-2))
   THEN (gProlong ⌜c⌝ ⌜a⌝ `x' ⌜c⌝ ⌜b⌝⋅ THENA Auto)
   THEN (gProlong ⌜c⌝ ⌜b⌝ `y' ⌜c⌝ ⌜a⌝⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. c # ba
6. x : Point
7. c_a_x ∧ ax ≅ cb
8. y : Point
9. c_b_y ∧ by ≅ ca
⊢ ∃f:Point. (acf ≅a bcf ∧ a-f-b)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  c  \#  ba\}  .    \mexists{}f:Point.  (acf  \mcong{}\msuba{}  bcf  \mwedge{}  a-f-b)


By

---

Latex:
((Auto  THEN  (Assert  c  \#  ba  BY  (DVar  `c'  THEN  Unhide  THEN  Auto))  THEN  D  -2  THEN  Thin  (-2))
  THEN  (gProlong  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}  `x'  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}  `y'  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index