---

Step * 1 2 of Lemma geo-parallel-symmetry


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. c ≠ d
8. ∀x:Point. (Colinear(a;b;x) ⇒ x # cd)
9. x : Point
10. Colinear(c;d;x)
11. x # ab ⇒ ((∀x@0:Point. (Colinear(x@0;a;b) ⇒ x ≠ x@0)) ∧ a ≠ b)
12. x2 : Point
13. Colinear(x2;a;b)
14. x2 # cd
15. d ≠ x
⊢ x ≠ x2
BY
{ (InstLemma `colinear-lsep` [⌜e⌝;⌜c⌝;⌜d⌝;⌜x2⌝;⌜x⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \mneq{}  b
7.  c  \mneq{}  d
8.  \mforall{}x:Point.  (Colinear(a;b;x)  {}\mRightarrow{}  x  \#  cd)
9.  x  :  Point
10.  Colinear(c;d;x)
11.  x  \#  ab  {}\mRightarrow{}  ((\mforall{}x@0:Point.  (Colinear(x@0;a;b)  {}\mRightarrow{}  x  \mneq{}  x@0))  \mwedge{}  a  \mneq{}  b)
12.  x2  :  Point
13.  Colinear(x2;a;b)
14.  x2  \#  cd
15.  d  \mneq{}  x
\mvdash{}  x  \mneq{}  x2


By

---

Latex:
(InstLemma  `colinear-lsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index