---

Step * of Lemma geo-intersect-symmetry

∀e:EuclideanPlane. ∀l,m:LINE.  (l \/ m ⇒ m \/ l)
BY
{ (Auto
   THEN (RWO "geo-intersect-iff2" (-1) THENA Auto)
   THEN ExRepD
   THEN (RWO "geo-intersect-iff2" 0 THENA Auto)
   THEN (InstConcl [⌜d⌝;⌜c⌝;⌜a⌝;⌜b⌝;⌜v⌝]⋅ THENA Auto)
   THEN SplitAndConcl
   THEN Try (Trivial)) }

1
1. e : EuclideanPlane
2. l : LINE
3. m : LINE
4. a : Point
5. b : Point
6. c : Point
7. d : Point
8. v : Point
9. a-v-b
10. c-v-d
11. a I l
12. b I l
13. c I m
14. d I m
15. a leftof cd
16. b leftof dc
17. c leftof ba
18. d leftof ab
⊢ d-v-c

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}l,m:LINE.    (l  \mbackslash{}/  m  {}\mRightarrow{}  m  \mbackslash{}/  l)


By

---

Latex:
(Auto
  THEN  (RWO  "geo-intersect-iff2"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO  "geo-intersect-iff2"  0  THENA  Auto)
  THEN  (InstConcl  [\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SplitAndConcl
  THEN  Try  (Trivial))

---

Home Index