---

Step * of Lemma right-angle_functionality

∀e:BasicGeometry. ∀a,b,c,a',b',c':Point.  (a ≡ a' ⇒ b ≡ b' ⇒ c ≡ c' ⇒ {Rabc ⇐⇒ Ra'b'c'})
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a ≡ a'
9. b ≡ b'
10. c ≡ c'
⊢ {Rabc ⇐⇒ Ra'b'c'}

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a',b',c':Point.    (a  \mequiv{}  a'  {}\mRightarrow{}  b  \mequiv{}  b'  {}\mRightarrow{}  c  \mequiv{}  c'  {}\mRightarrow{}  \{Rabc  \mLeftarrow{}{}\mRightarrow{}  Ra'b'c'\})


By

---

Latex:
Auto

---

Home Index