---

Step * 1 1 of Lemma geo-pt-swap-preserves-parallel

.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : a ≠ b
7. C : c ≠ d
8. A' : b ≠ a
9. <a, b, A> || <c, d, C>
⊢ <b, a, A'> ≡ <a, b, A>
BY
{ (BLemma `geo-colinear-line-eq2` THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  A  :  a  \mneq{}  b
7.  C  :  c  \mneq{}  d
8.  A'  :  b  \mneq{}  a
9.  <a,  b,  A>  ||  <c,  d,  C>
\mvdash{}  <b,  a,  A'>  \mequiv{}  <a,  b,  A>


By

---

Latex:
(BLemma  `geo-colinear-line-eq2`  THEN  Reduce  0  THEN  Auto)

---

Home Index