---

Step * of Lemma geo-lt-pt-exists

∀e:BasicGeometry. ∀a,b,c,d:Point.  (a ≠ b ⇒ ab < cd ⇒ (∃x:Point. (a-b-x ∧ ax ≅ cd)))
BY
{ (((Auto THEN Unfold `geo-lt-pt` -1) THEN D -1) THEN ExRepD) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. y : Point
8. c-y-d
9. ab ≅ cy
⊢ ∃x:Point. (a-b-x ∧ ax ≅ cd)

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    (a  \mneq{}  b  {}\mRightarrow{}  ab  <  cd  {}\mRightarrow{}  (\mexists{}x:Point.  (a-b-x  \mwedge{}  ax  \00D0  cd)))


By

---

Latex:
(((Auto  THEN  Unfold  `geo-lt-pt`  -1)  THEN  D  -1)  THEN  ExRepD)

---

Home Index