---

Step * of Lemma geo-between-same-side2-or-strong

∀e:BasicGeometry. ∀A,B,C,d:Point.  ((A ≠ B ∧ C ≠ d) ⇒ A_B_C ⇒ A_B_d ⇒ (B_C_d ∨ B_d_C))
BY
{ ((UnivCD THENA Auto) THEN InstLemma `geo-between-same-side-or` [⌜e⌝;⌜A⌝;⌜B⌝;⌜C⌝;⌜d⌝]⋅ THEN Auto) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. d : Point
6. A ≠ B
7. C ≠ d
8. A_B_C
9. A_B_d
10. A_C_d ∨ A_d_C
⊢ B_C_d ∨ B_d_C

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,C,d:Point.    ((A  \mneq{}  B  \mwedge{}  C  \mneq{}  d)  {}\mRightarrow{}  A\_B\_C  {}\mRightarrow{}  A\_B\_d  {}\mRightarrow{}  (B\_C\_d  \mvee{}  B\_d\_C))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  InstLemma  `geo-between-same-side-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index