---

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

.....assertion..... 
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> ∈ LINE
BY
{ (EqTypeCD THEN Auto) }

1
.....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>

---

Latex:

---

Latex:
.....assertion..... 
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'>  =  <a,  b,  A>


By

---

Latex:
(EqTypeCD  THEN  Auto)

---

Home Index