---

Step * 7 1 of Lemma eu-eq_dist-axiomsA


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. a' : Point
11. b' : Point
12. c' : Point
13. u : {u:Point| c' # u} 
14. B(a'b'c')
15. B(a'uc')
16. ab ≅ a'b'
17. cd ≅ b'c'
18. ef ≅ a'u
19. ¬D(x;y;y;y;e;f)
20. ¬xy > ef
21. ef ≥ xy
⊢ ∃a',b',c':Point. ∃u:{u:Point| c' # u} . (B(a'b'c') ∧ B(a'uc') ∧ ab ≅ a'b' ∧ cd ≅ b'c' ∧ xy ≅ a'u)
BY
{ ((Assert a' # c' BY
          ((InstLemma `geo-between-sep` [⌜g⌝;⌜c'⌝;⌜a'⌝;⌜u⌝]⋅ THEN Auto) THEN (D 13 THEN Unhide) THEN Auto))
   THEN (gProperProlong ⌜c'⌝⌜a'⌝`B'⌜c'⌝⌜a'⌝⋅ THENA Auto)
   THEN (gProlong ⌜B⌝⌜a'⌝`t'⌜x⌝⌜y⌝⋅ THENA Auto)
   THEN ExRepD) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. a' : Point
11. b' : Point
12. c' : Point
13. u : {u:Point| c' # u} 
14. B(a'b'c')
15. B(a'uc')
16. ab ≅ a'b'
17. cd ≅ b'c'
18. ef ≅ a'u
19. ¬D(x;y;y;y;e;f)
20. ¬xy > ef
21. ef ≥ xy
22. a' # c'
23. B : Point
24. c'-a'-B
25. a'B ≅ c'a'
26. t : Point
27. B(Ba't)
28. a't ≅ xy
⊢ ∃a',b',c':Point. ∃u:{u:Point| c' # u} . (B(a'b'c') ∧ B(a'uc') ∧ ab ≅ a'b' ∧ cd ≅ b'c' ∧ xy ≅ a'u)

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  x  :  Point
9.  y  :  Point
10.  a'  :  Point
11.  b'  :  Point
12.  c'  :  Point
13.  u  :  \{u:Point|  c'  \#  u\} 
14.  B(a'b'c')
15.  B(a'uc')
16.  ab  \mcong{}  a'b'
17.  cd  \mcong{}  b'c'
18.  ef  \mcong{}  a'u
19.  \mneg{}D(x;y;y;y;e;f)
20.  \mneg{}xy  >  ef
21.  ef  \mgeq{}  xy
\mvdash{}  \mexists{}a',b',c':Point.  \mexists{}u:\{u:Point|  c'  \#  u\}  .  (B(a'b'c')  \mwedge{}  B(a'uc')  \mwedge{}  ab  \mcong{}  a'b'  \mwedge{}  cd  \mcong{}  b'c'  \mwedge{}  xy  \mcong{}  a'u)


By

---

Latex:
((Assert  a'  \#  c'  BY
                ((InstLemma  `geo-between-sep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  THEN  (D  13  THEN  Unhide)
                  THEN  Auto))
  THEN  (gProperProlong  \mkleeneopen{}c'\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}`B'\mkleeneopen{}c'\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}B\mkleeneclose{}\mkleeneopen{}a'\mkleeneclose{}`t'\mkleeneopen{}x\mkleeneclose{}\mkleeneopen{}y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index