---

Step * 1 1 1 1 1 2 1 of Lemma Euclid-Prop2-lemma


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a # b
5. v : Point
6. c : Point
7. cb ≅ ab
8. ca ≅ ba
9. ca ≅ cb
10. c leftof ab
11. y : Point
12. B(cbc)
13. bc ≅ bv
14. v1 : Point
15. cv1 ≅ cc
16. B(acv1)
17. c # c ⇒ c # v1
18. x : Point
19. cc ≅ cc
20. B(ccv1)
21. Colinear(a;c;c)
22. c # c ⇒ c # v1
23. Colinear(c;a;c)
24. x ≡ c
25. y ≡ c
⊢ B(cac)
BY
{ (FLemma `geo-between-same` [12] THENA Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a # b
5. v : Point
6. c : Point
7. cb ≅ ab
8. ca ≅ ba
9. ca ≅ cb
10. c leftof ab
11. y : Point
12. B(cbc)
13. bc ≅ bv
14. v1 : Point
15. cv1 ≅ cc
16. B(acv1)
17. c # c ⇒ c # v1
18. x : Point
19. cc ≅ cc
20. B(ccv1)
21. Colinear(a;c;c)
22. c # c ⇒ c # v1
23. Colinear(c;a;c)
24. x ≡ c
25. y ≡ c
26. c ≡ b
⊢ B(cac)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  a  \#  b
5.  v  :  Point
6.  c  :  Point
7.  cb  \mcong{}  ab
8.  ca  \mcong{}  ba
9.  ca  \mcong{}  cb
10.  c  leftof  ab
11.  y  :  Point
12.  B(cbc)
13.  bc  \mcong{}  bv
14.  v1  :  Point
15.  cv1  \mcong{}  cc
16.  B(acv1)
17.  c  \#  c  {}\mRightarrow{}  c  \#  v1
18.  x  :  Point
19.  cc  \mcong{}  cc
20.  B(ccv1)
21.  Colinear(a;c;c)
22.  c  \#  c  {}\mRightarrow{}  c  \#  v1
23.  Colinear(c;a;c)
24.  x  \mequiv{}  c
25.  y  \mequiv{}  c
\mvdash{}  B(cac)


By

---

Latex:
(FLemma  `geo-between-same`  [12]  THENA  Auto)

---

Home Index