---

Step * 2 1 1 1 1 1 of Lemma geo-lt-implies-gt


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ∃a@0,b@0:Point. (a@0 ≠ b@0 ∧ 0 + |a@0b@0| ≤ |ab|)
7. c ≡ d
8. |cd| = 0 ∈ Length
9. c ≡ d
10. a_a_b
11. aa ≅ dd
⊢ a ≠ b
BY
{ ((ExRepD THEN InstLemma `geo-le-sep` [⌜g⌝;⌜a@0⌝;⌜b@0⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto)
   THEN (Assert 0 + |a@0b@0| = |a@0b@0| ∈ Length BY
               Auto)
   THEN RWO "-1" 9
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  \mexists{}a@0,b@0:Point.  (a@0  \mneq{}  b@0  \mwedge{}  0  +  |a@0b@0|  \mleq{}  |ab|)
7.  c  \mequiv{}  d
8.  |cd|  =  0
9.  c  \mequiv{}  d
10.  a\_a\_b
11.  aa  \mcong{}  dd
\mvdash{}  a  \mneq{}  b


By

---

Latex:
((ExRepD  THEN  InstLemma  `geo-le-sep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a@0\mkleeneclose{};\mkleeneopen{}b@0\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (Assert  0  +  |a@0b@0|  =  |a@0b@0|  BY
                          Auto)
  THEN  RWO  "-1"  9
  THEN  Auto)

---

Home Index