---

Step * 5 of Lemma eu-colinear-transitivity


1. e : EuclideanPlane
2. A : Point
3. C : Point
4. B : Point
5. D : Point
6. Colinear(B;C;D)
7. ¬(B = C ∈ Point)
8. ¬(A = B ∈ Point)
9. A-C-B
10. ¬(B = C ∈ Point)
11. B-C-D
⊢ Colinear(A;B;D)
BY
{ (AddBetweenEqFacts
   THEN ((BLemma `eu-colinear-permute` THEN Auto) THEN BLemma `eu-colinear-swap` THEN Auto)
   THEN BinaryForwardChain (ioid Obid: eu-colinear-same-side2)⋅) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  A  :  Point
3.  C  :  Point
4.  B  :  Point
5.  D  :  Point
6.  Colinear(B;C;D)
7.  \mneg{}(B  =  C)
8.  \mneg{}(A  =  B)
9.  A-C-B
10.  \mneg{}(B  =  C)
11.  B-C-D
\mvdash{}  Colinear(A;B;D)


By

---

Latex:
(AddBetweenEqFacts
  THEN  ((BLemma  `eu-colinear-permute`  THEN  Auto)  THEN  BLemma  `eu-colinear-swap`  THEN  Auto)
  THEN  BinaryForwardChain  (ioid  Obid:  eu-colinear-same-side2)\mcdot{})

---

Home Index