---

Step * of Lemma extended-out-preserves-between

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d:Point.  ((out(a bc) ∧ b-a-d) ⇒ c-a-d)
BY
{ ((Auto THEN gProperProlong ⌜d⌝⌜a⌝`C'⌜a⌝⌜c⌝⋅ THEN Auto) THEN (Assert out(a bC) BY Auto)) }

1
.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. out(a bc)
7. b-a-d
8. C : Point
9. d-a-C
10. aC ≅ ac
⊢ out(a bC)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. out(a bc)
7. b-a-d
8. C : Point
9. d-a-C
10. aC ≅ ac
11. out(a bC)
⊢ c-a-d

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    ((out(a  bc)  \mwedge{}  b-a-d)  {}\mRightarrow{}  c-a-d)


By

---

Latex:
((Auto  THEN  gProperProlong  \mkleeneopen{}d\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`C'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  (Assert  out(a  bC)  BY  Auto))

---

Home Index