---

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

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

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. ¬((¬A_C_D) ∧ (¬A_D_C))
10. ¬A-C-D
11. ¬A-D-C
⊢ False

---

Latex:

---

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


By

---

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

---

Home Index