---

Step * of Lemma geo-intersect-points-symmetry

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab \/ cd ⇒ cd \/ ab)
BY
{ (Auto
   THEN (RWO "geo-intersect-points-iff" (-1) THENA Auto)
   THEN ExRepD
   THEN (RWO "geo-intersect-points-iff" 0 THENA Auto)
   THEN GenRepD) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. c ≠ d
8. a1 : Point
9. b1 : Point
10. c1 : Point
11. d1 : Point
12. v : Point
13. a1-v-b1
14. c1-v-d1
15. Colinear(a1;a;b)
16. Colinear(b1;a;b)
17. Colinear(c1;c;d)
18. Colinear(d1;c;d)
19. a1 leftof c1d1
20. b1 leftof d1c1
⊢ ∃a1,b1,c1,d1,v:Point
   (a1-v-b1
   ∧ c1-v-d1
   ∧ Colinear(a1;c;d)
   ∧ Colinear(b1;c;d)
   ∧ Colinear(c1;a;b)
   ∧ Colinear(d1;a;b)
   ∧ a1 leftof c1d1
   ∧ b1 leftof d1c1)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab  \mbackslash{}/  cd  {}\mRightarrow{}  cd  \mbackslash{}/  ab)


By

---

Latex:
(Auto
  THEN  (RWO  "geo-intersect-points-iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO  "geo-intersect-points-iff"  0  THENA  Auto)
  THEN  GenRepD)

---

Home Index