---

Step * 2 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 = C ∈ Point)
9. ¬(A = B ∈ Point)
10. A-C-B
11. ¬(B = C ∈ Point)
12. B-C-D
⊢ Colinear(A;C;D)
BY
{ (AddBetweenEqFacts
   THEN (BLemma `eu-colinear-swap` THENA Auto)
   THEN BinaryForwardChain (ioid Obid: eu-colinear-same-side)⋅) }

---

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  =  C)
9.  \mneg{}(A  =  B)
10.  A-C-B
11.  \mneg{}(B  =  C)
12.  B-C-D
\mvdash{}  Colinear(A;C;D)


By

---

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

---

Home Index