---

Step * of Lemma adjacent-right-angles-supplementary-using-geom-tactic

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (c-b-d ⇒ a ≠ b ⇒ (Rabc ⇐⇒ abc ≅a abd))
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a ≠ b
8. Rabc
⊢ abc ≅a abd

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c-b-d
7. a ≠ b
8. abc ≅a abd
⊢ Rabc

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (c-b-d  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  (Rabc  \mLeftarrow{}{}\mRightarrow{}  abc  \mcong{}\msuba{}  abd))


By

---

Latex:
Auto

---

Home Index