---

Step * of Lemma geo-between-exchange4

∀e:BasicGeometry-. ∀[a,b,c,d:Point].  (a_b_d) supposing (a_c_d and a_b_c)
BY
{ (Auto THEN gSeparatedCases ⌜b⌝ ⌜c⌝⋅ THEN Auto) }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a_b_c
7. a_c_d
8. b ≠ c
⊢ a_b_d

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry-.  \mforall{}[a,b,c,d:Point].    (a\_b\_d)  supposing  (a\_c\_d  and  a\_b\_c)


By

---

Latex:
(Auto  THEN  gSeparatedCases  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index