---

Step * of Lemma Euclid-Prop7-aux

No Annotations
∀e:EuclideanPlane. ∀a,b:Point. ∀c,d:{p:Point| ¬p leftof ba} .  (a # b ⇒ ac ≅ ad ⇒ bc ≅ bd ⇒ c ≡ d)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (InstLemma `Euclid-midpoint` [⌜e⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `m' (-2)
   THEN D -1
   THEN (InstLemma `upper-dimension-axiom` [⌜e⌝;⌜a⌝;⌜b⌝;⌜m⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : {c:Point| ¬c leftof ba} 
5. d : {p:Point| ¬p leftof ba} 
6. a # b
7. ac ≅ ad
8. bc ≅ bd
9. c # d
10. m : Point
11. B(cmd)
12. cm ≅ md
13. Colinear(a;b;m)
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c,d:\{p:Point|  \mneg{}p  leftof  ba\}  .    (a  \#  b  {}\mRightarrow{}  ac  \mcong{}  ad  {}\mRightarrow{}  bc  \mcong{}  bd  {}\mRightarrow{}  c  \mequiv{}  d\000C)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `Euclid-midpoint`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `m'  (-2)
  THEN  D  -1
  THEN  (InstLemma  `upper-dimension-axiom`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index