---

Step * 8 1 1 1 1 1 of Lemma eu-eq_dist-axiomsA

.....aux..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. a' : Point
9. c' : Point
10. A : Point
11. B : Point
12. E1 : Point
13. E2 : Point
14. C : Point
15. xy ≥ ab
16. c'-a'-A
17. B(Aa'B)
18. a'B ≅ xy
19. c'E1 ≅ xy
20. c'E2 ≅ cd
21. B(Aa'C)
22. a'C ≅ E1E2
23. B(E1c'E2)
24. a' # B
25. a' # C
⊢ B(a'BC)
BY
{ ((InstLemma `geo-out-le-iff-bet` [⌜g⌝;⌜a'⌝;⌜B⌝;⌜C⌝]⋅ THENA Auto)
   THENA (InstLemma `geo-out-iff-between1` [⌜g⌝;⌜a'⌝;⌜B⌝;⌜C⌝;⌜A⌝]⋅ THEN Auto)
   ) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. a' : Point
9. c' : Point
10. A : Point
11. B : Point
12. E1 : Point
13. E2 : Point
14. C : Point
15. xy ≥ ab
16. c'-a'-A
17. B(Aa'B)
18. a'B ≅ xy
19. c'E1 ≅ xy
20. c'E2 ≅ cd
21. B(Aa'C)
22. a'C ≅ E1E2
23. B(E1c'E2)
24. a' # B
25. a' # C
26. |a'B| ≤ |a'C| ⇐⇒ B(a'BC)
⊢ B(a'BC)

---

Latex:

---

Latex:
.....aux..... 
1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  x  :  Point
7.  y  :  Point
8.  a'  :  Point
9.  c'  :  Point
10.  A  :  Point
11.  B  :  Point
12.  E1  :  Point
13.  E2  :  Point
14.  C  :  Point
15.  xy  \mgeq{}  ab
16.  c'-a'-A
17.  B(Aa'B)
18.  a'B  \mcong{}  xy
19.  c'E1  \mcong{}  xy
20.  c'E2  \mcong{}  cd
21.  B(Aa'C)
22.  a'C  \mcong{}  E1E2
23.  B(E1c'E2)
24.  a'  \#  B
25.  a'  \#  C
\mvdash{}  B(a'BC)


By

---

Latex:
((InstLemma  `geo-out-le-iff-bet`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THENA  (InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THEN  Auto)
  )

---

Home Index