---

Step * 1 1 of Lemma geo-SS_functionality


1. g : EuclideanPlane
2. v' : Point
3. u' : Point
4. b' : Point
5. a' : Point
6. u' leftof a'b'
7. v' leftof b'a'
8. u' leftof a'b'
9. v' leftof b'a'
10. v1 : Point
11. Colinear(a';b';v1)
12. B(u'v1v')
13. v2 : Point
14. Colinear(a';b';v2)
15. B(u'v2v')
⊢ v1 ≡ v2
BY
{ (InstLemma `geo-intersection-unicity` [⌜g⌝;⌜a'⌝;⌜b'⌝;⌜u'⌝;⌜v'⌝;⌜v1⌝;⌜v2⌝]⋅
   THEN Auto
   THEN Try ((RWO "not-lsep-iff-colinear<" 0 THEN Auto))) }

1
.....antecedent..... 
1. g : EuclideanPlane
2. v' : Point
3. u' : Point
4. b' : Point
5. a' : Point
6. u' leftof a'b'
7. v' leftof b'a'
8. u' leftof a'b'
9. v' leftof b'a'
10. v1 : Point
11. Colinear(a';b';v1)
12. B(u'v1v')
13. v2 : Point
14. Colinear(a';b';v2)
15. B(u'v2v')
⊢ u' # v'

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  v'  :  Point
3.  u'  :  Point
4.  b'  :  Point
5.  a'  :  Point
6.  u'  leftof  a'b'
7.  v'  leftof  b'a'
8.  u'  leftof  a'b'
9.  v'  leftof  b'a'
10.  v1  :  Point
11.  Colinear(a';b';v1)
12.  B(u'v1v')
13.  v2  :  Point
14.  Colinear(a';b';v2)
15.  B(u'v2v')
\mvdash{}  v1  \mequiv{}  v2


By

---

Latex:
(InstLemma  `geo-intersection-unicity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}u'\mkleeneclose{};\mkleeneopen{}v'\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((RWO  "not-lsep-iff-colinear<"  0  THEN  Auto)))

---

Home Index