Step * of Lemma lt-angle-implies-between-if-out

No Annotations
e:EuclideanPlane. ∀a,b,c,d:Point.  (a bc  bad < bac  out(b dc)  b-d-c)
BY
(Auto THEN (D THENA Auto)) }

1
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. bc
7. bad < bac
8. out(b dc)
⊢ B(bdc)

2
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. bc
7. bad < bac
8. out(b dc)
⊢ d ∧ c


Latex:


Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (a  \#  bc  {}\mRightarrow{}  bad  <  bac  {}\mRightarrow{}  out(b  dc)  {}\mRightarrow{}  b-d-c)


By


Latex:
(Auto  THEN  (D  0  THENA  Auto))




Home Index