---

Step * 1 of Lemma geo-le-pt-transitivity


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c' : Point
7. d' : Point
8. a ≠ b
9. y1 : Point
10. c_y1_d
11. ab ≅ cy1
12. y : Point
13. c'_y_d'
14. cd ≅ c'y
15. ∃b':Point. (c'_b'_y ∧ cy1 ≅ c'b' ∧ y1d ≅ b'y)
⊢ ∃y:Point. (c'_y_d' ∧ ab ≅ c'y)
BY
{ ((D -1 THEN ExRepD) THEN InstConcl [⌜b'⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  c'  :  Point
7.  d'  :  Point
8.  a  \mneq{}  b
9.  y1  :  Point
10.  c\_y1\_d
11.  ab  \00D0  cy1
12.  y  :  Point
13.  c'\_y\_d'
14.  cd  \00D0  c'y
15.  \mexists{}b':Point.  (c'\_b'\_y  \mwedge{}  cy1  \00D0  c'b'  \mwedge{}  y1d  \00D0  b'y)
\mvdash{}  \mexists{}y:Point.  (c'\_y\_d'  \mwedge{}  ab  \00D0  c'y)


By

---

Latex:
((D  -1  THEN  ExRepD)  THEN  InstConcl  [\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index