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