---

Step * of Lemma between-implies-straightangle

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

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a-b-c
9. abc ≅a a'b'c'
10. a' ≠ b'
11. b' ≠ c'
⊢ a'-b'-c'

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a-b-c
9. a'-b'-c'
⊢ abc ≅a a'b'c'

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index