---

Step * 1 of Lemma geo-SS_functionality


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. u : {u:Point| u leftof ab} 
5. v : {v:Point| v leftof ba} 
6. a' : Point
7. b' : Point
8. u' : {u:Point| u leftof a'b'} 
9. v' : {v:Point| v leftof b'a'} 
10. a ≡ a'
11. b ≡ b'
12. u ≡ u'
13. v ≡ v'
14. v1 : Point
15. Colinear(a;b;v1)
16. B(uv1v)
17. v2 : Point
18. Colinear(a';b';v2)
19. B(u'v2v')
⊢ v1 ≡ v2
BY
{ (DSetVars⋅
   THEN (Unhide THENA Auto)
   THEN ((gEliminatePoint 14⋅ THENA Auto) THEN ThinVar `a')
   THEN ((gEliminatePoint 13⋅ THENA Auto) THEN ThinVar `b')
   THEN ((gEliminatePoint 12⋅ THENA Auto) THEN ThinVar `u')
   THEN (gEliminatePoint 11⋅ THENA Auto)
   THEN ThinVar `v') }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
(DSetVars\mcdot{}
  THEN  (Unhide  THENA  Auto)
  THEN  ((gEliminatePoint  14\mcdot{}  THENA  Auto)  THEN  ThinVar  `a')
  THEN  ((gEliminatePoint  13\mcdot{}  THENA  Auto)  THEN  ThinVar  `b')
  THEN  ((gEliminatePoint  12\mcdot{}  THENA  Auto)  THEN  ThinVar  `u')
  THEN  (gEliminatePoint  11\mcdot{}  THENA  Auto)
  THEN  ThinVar  `v')

---

Home Index