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. EuclideanPlane
2. Point
3. Point
4. 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. EuclideanPlane
2. Point
3. Point
4. 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