---

Step * of Lemma geo-strict-between-same-side2

∀e:BasicGeometry. ∀[A,B,C,D:Point].  (¬((¬B-C-D) ∧ (¬B-D-C))) supposing (C ≠ D and A-B-C and A-B-D)
BY
{ (((Auto THEN (InstLemma `geo-between-same-side2` [⌜e⌝;⌜A⌝;⌜B⌝;⌜C⌝;⌜D⌝]⋅ THENM D 0)) THENA Auto)
   THEN D -1
   THEN D -3
   THEN D 0) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. A-B-D
7. A-B-C
8. C ≠ D
9. ¬B-C-D
10. ¬B-D-C
⊢ ¬B_C_D

2
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. A-B-D
7. A-B-C
8. C ≠ D
9. ¬B-C-D
10. ¬B-D-C
⊢ ¬B_D_C

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[A,B,C,D:Point].    (\mneg{}((\mneg{}B-C-D)  \mwedge{}  (\mneg{}B-D-C)))  supposing  (C  \mneq{}  D  and  A-B-C  and  A-B-D)


By

---

Latex:
(((Auto  THEN  (InstLemma  `geo-between-same-side2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{}]\mcdot{}  THENM  D  0))  THENA  Auto)
  THEN  D  -1
  THEN  D  -3
  THEN  D  0)

---

Home Index