---

Step * of Lemma geo-double-pasch-same-point

∀e:HeytingGeometry. ∀A,B,C,d,f,g,x,y:Point.
  (A # BC ⇒ A-d-C ⇒ A-g-B ⇒ B-f-C ⇒ C-x-g ⇒ C-y-g ⇒ B-x-d ⇒ B-y-d ⇒ A-x-f ⇒ A-y-f ⇒ x ≡ y)
BY
{ Auto }

1
1. e : HeytingGeometry
2. A : Point
3. B : Point
4. C : Point
5. d : Point
6. f : Point
7. g : Point
8. x : Point
9. y : Point
10. A # BC
11. A-d-C
12. A-g-B
13. B-f-C
14. C-x-g
15. C-y-g
16. B-x-d
17. B-y-d
18. A-x-f
19. A-y-f
⊢ x ≡ y

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}A,B,C,d,f,g,x,y:Point.
    (A  \#  BC  {}\mRightarrow{}  A-d-C  {}\mRightarrow{}  A-g-B  {}\mRightarrow{}  B-f-C  {}\mRightarrow{}  C-x-g  {}\mRightarrow{}  C-y-g  {}\mRightarrow{}  B-x-d  {}\mRightarrow{}  B-y-d  {}\mRightarrow{}  A-x-f  {}\mRightarrow{}  A-y-f  {}\mRightarrow{}  x  \mequiv{}  y)


By

---

Latex:
Auto

---

Home Index