---

Step * of Lemma geo-le-cases2

∀e:BasicGeometry. ∀[p,q:Length].  (¬¬((p < q ∨ q < p) ∨ (p = q ∈ Length)))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (UseWitness ⌜Ax⌝⋅ THEN (D 3 THEN D 2) THEN Assert ⌜False⌝⋅ THEN Auto)
   THEN (MoveToConcl (-1)
         THEN (GenConcl ⌜p = a ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto)
         THEN (GenConcl ⌜q = b ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto)
         THEN All Thin)
   THEN (Assert {p:Point| B(OXp)}  ⊆r Length BY
               (Unfold `geo-length-type` 0 THEN Auto))
   THEN (D 0 THENA Auto)
   THEN ((Assert (a ∈ Length) ∧ (b ∈ Length) BY Auto) THEN DSetVars)
   THEN (FLemma `geo-between-same-side2` [3;5] THENA Auto)
   THEN D -1
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN gSeparatedCases ⌜a⌝⌜b⌝⋅
   THEN Auto) }

1
1. e : BasicGeometry
2. a : Point
3. B(OXa)
4. b : Point
5. B(OXb)
6. {p:Point| B(OXp)}  ⊆r Length
7. ¬((a < b ∨ b < a) ∨ (a = b ∈ Length))
8. a ∈ Length
9. b ∈ Length
10. B(Xba)
11. a # b
⊢ False

2
1. e : BasicGeometry
2. b : Point
3. a : Point
4. B(OXb)
5. B(OXb)
6. {p:Point| B(OXp)}  ⊆r Length
7. ¬((a < b ∨ b < a) ∨ (a = b ∈ Length))
8. a ∈ Length
9. b ∈ Length
10. B(Xbb)
11. a ≡ b
⊢ False

3
1. e : BasicGeometry
2. a : Point
3. B(OXa)
4. b : Point
5. B(OXb)
6. {p:Point| B(OXp)}  ⊆r Length
7. ¬((a < b ∨ b < a) ∨ (a = b ∈ Length))
8. a ∈ Length
9. b ∈ Length
10. B(Xab)
11. a # b
⊢ False

4
1. e : BasicGeometry
2. b : Point
3. a : Point
4. B(OXb)
5. B(OXb)
6. {p:Point| B(OXp)}  ⊆r Length
7. ¬((a < b ∨ b < a) ∨ (a = b ∈ Length))
8. a ∈ Length
9. b ∈ Length
10. B(Xbb)
11. a ≡ b
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}[p,q:Length].    (\mneg{}\mneg{}((p  <  q  \mvee{}  q  <  p)  \mvee{}  (p  =  q)))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  (D  3  THEN  D  2)  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (MoveToConcl  (-1)
              THEN  (GenConcl  \mkleeneopen{}p  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (GenConcl  \mkleeneopen{}q  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  All  Thin)
  THEN  (Assert  \{p:Point|  B(OXp)\}    \msubseteq{}r  Length  BY
                          (Unfold  `geo-length-type`  0  THEN  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  ((Assert  (a  \mmember{}  Length)  \mwedge{}  (b  \mmember{}  Length)  BY  Auto)  THEN  DSetVars)
  THEN  (FLemma  `geo-between-same-side2`  [3;5]  THENA  Auto)
  THEN  D  -1
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index