---

Step * of Lemma geo-between-outer-trans

No Annotations
∀e:BasicGeometry-. ∀[a,b,c,d:Point].  (B(acd)) supposing (B(bcd) and B(abc) and b # c)
BY
{ (Auto THEN gSeparatedCases ⌜a⌝ ⌜c⌝⋅ THEN Auto) }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b # c
7. B(abc)
8. B(bcd)
9. a # c
⊢ B(acd)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry-.  \mforall{}[a,b,c,d:Point].    (B(acd))  supposing  (B(bcd)  and  B(abc)  and  b  \#  c)


By

---

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

---

Home Index