---

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

∀e:EuclideanPlane. ∀a,b,c,d:Point. ∀A:a ≠ b. ∀C:c ≠ d. ∀A':b ≠ a.  (<a, b, A> || <c, d, C> ⇒ <b, a, A'> || <c, d, C>)
BY
{ (Auto THEN (Assert ⌜<b, a, A'> = <a, b, A> ∈ LINE⌝⋅ THENM (RWO  "-1" 0 THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.  \mforall{}A:a  \mneq{}  b.  \mforall{}C:c  \mneq{}  d.  \mforall{}A':b  \mneq{}  a.
    (<a,  b,  A>  ||  <c,  d,  C>  {}\mRightarrow{}  <b,  a,  A'>  ||  <c,  d,  C>)


By

---

Latex:
(Auto  THEN  (Assert  \mkleeneopen{}<b,  a,  A'>  =  <a,  b,  A>\mkleeneclose{}\mcdot{}  THENM  (RWO    "-1"  0  THEN  Auto)))

---

Home Index