---

Step * of Lemma le-if-point-be-end

∀e:BasicGeometry. ∀a,b,c,d,x:Point.  (a ≠ b ⇒ a_b_x ⇒ ax ≅ cd ⇒ ab≤cd)
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. a ≠ b
8. a_b_x
9. ax ≅ cd
⊢ ab≤cd

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d,x:Point.    (a  \mneq{}  b  {}\mRightarrow{}  a\_b\_x  {}\mRightarrow{}  ax  \00D0  cd  {}\mRightarrow{}  ab\mleq{}cd)


By

---

Latex:
Auto

---

Home Index