---

Step * 1 of Lemma geo-parallel-symmetry


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b ∧ c ≠ d
7. ∀x:Point. (Colinear(a;b;x) ⇒ x # cd)
8. x : Point
9. Colinear(c;d;x)
⊢ x # ab
BY
{ (((InstLemma `lsep-iff-all-sep` [⌜e⌝;⌜x⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
    THEN (RepeatFor 2 (D -1) THEN Auto)
    THEN (RenameVar `x2' (12) THEN Auto)
    THEN InstHyp [⌜x2⌝] (8)⋅
    THEN Auto)
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜c⌝;⌜d⌝;⌜x⌝]⋅ THEN Auto)
   THEN D -1) }

1
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. c ≠ x
⊢ x ≠ x2

2
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

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \mneq{}  b  \mwedge{}  c  \mneq{}  d
7.  \mforall{}x:Point.  (Colinear(a;b;x)  {}\mRightarrow{}  x  \#  cd)
8.  x  :  Point
9.  Colinear(c;d;x)
\mvdash{}  x  \#  ab


By

---

Latex:
(((InstLemma  `lsep-iff-all-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (RepeatFor  2  (D  -1)  THEN  Auto)
    THEN  (RenameVar  `x2'  (12)  THEN  Auto)
    THEN  InstHyp  [\mkleeneopen{}x2\mkleeneclose{}]  (8)\mcdot{}
    THEN  Auto)
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  D  -1)

---

Home Index