---

Step * of Lemma Euclid-Prop7

No Annotations
∀e:EuclideanPlane. ∀a,b:Point. ∀c,d:{p:Point| p leftof ab} .  (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) }

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

---

Latex:

---

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


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)

---

Home Index