---

Step * of Lemma Euclid-prop13

∀g:EuclideanPlane. ∀a,b,c,d:Point.  (c-b-d ⇒ a # cd ⇒ abc + abd ≅ cbd)
BY
{ (Auto THEN Assert ⌜a ≠ b⌝⋅) }

1
.....assertion..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a # cd
⊢ a ≠ b

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a # cd
8. a ≠ b
⊢ abc + abd ≅ cbd

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (c-b-d  {}\mRightarrow{}  a  \#  cd  {}\mRightarrow{}  abc  +  abd  \mcong{}  cbd)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}a  \mneq{}  b\mkleeneclose{}\mcdot{})

---

Home Index