---

Step * of Lemma geo-ge-between-sep

∀g:EuclideanPlane. ∀a,b,c,a1,a2,x,y,t:Point.  (a_b_c ⇒ b ≠ c ⇒ ab ≅ a1a2 ⇒ a1a2 ≥ xy ⇒ a_t_c ⇒ at ≅ xy ⇒ t ≠ c)
BY
{ Auto }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a1 : Point
6. a2 : Point
7. x : Point
8. y : Point
9. t : Point
10. a_b_c
11. b ≠ c
12. ab ≅ a1a2
13. a1a2 ≥ xy
14. a_t_c
15. at ≅ xy
⊢ t ≠ c

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,a1,a2,x,y,t:Point.
    (a\_b\_c  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  ab  \mcong{}  a1a2  {}\mRightarrow{}  a1a2  \mgeq{}  xy  {}\mRightarrow{}  a\_t\_c  {}\mRightarrow{}  at  \mcong{}  xy  {}\mRightarrow{}  t  \mneq{}  c)


By

---

Latex:
Auto

---

Home Index