---

Step * 1 1 1 of Lemma geo-SS_functionality

.....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'
BY
{ (FLemma `left-right-sep` [6;7] THEN Auto) }

---

Latex:

---

Latex:
.....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')
\mvdash{}  u'  \#  v'


By

---

Latex:
(FLemma  `left-right-sep`  [6;7]  THEN  Auto)

---

Home Index