---

Step * of Lemma Euclid-Prop7'

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d:Point.  (a # b ⇒ ac ≅ ad ⇒ bc ≅ bd ⇒ (¬c leftof ba ⇐⇒ ¬d leftof ba) ⇒ 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 : Point
5. d : Point
6. a # b
7. ac ≅ ad
8. bc ≅ bd
9. (¬c leftof ba) ⇒ (¬d leftof ba)
10. (¬c leftof ba) ⇐ ¬d leftof ba
11. c # d
12. m : Point
13. B(cmd)
14. cm ≅ md
15. Colinear(a;b;m)
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.
    (a  \#  b  {}\mRightarrow{}  ac  \mcong{}  ad  {}\mRightarrow{}  bc  \mcong{}  bd  {}\mRightarrow{}  (\mneg{}c  leftof  ba  \mLeftarrow{}{}\mRightarrow{}  \mneg{}d  leftof  ba)  {}\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
  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