---

Step * of Lemma not-dist-cong

∀g:EuclideanPlane. ∀a,b,c,d:Point.  (((¬D(a;b;b;b;c;d)) ∧ (¬D(c;d;d;d;a;b))) ⇒ ab ≅ cd)
BY
{ ((Auto THEN (InstLemma `not-dist-lemma` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto))
   THEN (InstLemma `not-dist-lemma` [⌜g⌝;⌜c⌝;⌜d⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   ) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ¬D(a;b;b;b;c;d)
7. ¬D(c;d;d;d;a;b)
8. ¬ab > cd
9. ¬cd > ab
⊢ ab ≅ cd

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (((\mneg{}D(a;b;b;b;c;d))  \mwedge{}  (\mneg{}D(c;d;d;d;a;b)))  {}\mRightarrow{}  ab  \mcong{}  cd)


By

---

Latex:
((Auto  THEN  (InstLemma  `not-dist-lemma`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (InstLemma  `not-dist-lemma`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index