---

Step * of Lemma out-implies-straightangle

∀e:EuclideanPlane. ∀a,b,c,a',b',c':Point.  (a' ≠ b' ⇒ c' ≠ b' ⇒ out(b ac) ⇒ (abc ≅a a'b'c' ⇐⇒ out(b' a'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'
9. c' ≠ b'
10. out(b ac)
11. abc ≅a a'b'c'
⊢ out(b' a'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'
9. c' ≠ b'
10. out(b ac)
11. out(b' a'c')
⊢ abc ≅a a'b'c'

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index