---

Step * 1 of Lemma pgeo-primitives_wf


"Point":Type
"Line":Type
"PS":Point ⟶ self."Line" ⟶ ℙ ∈ 𝕌'
BY
{ Unfold `pgeo-point` 0 }

1
"Point":Type
"Line":Type
"PS":self."Point" ⟶ self."Line" ⟶ ℙ ∈ 𝕌'

---

Latex:

---

Latex:

"Point":Type
"Line":Type
"PS":Point  {}\mrightarrow{}  self."Line"  {}\mrightarrow{}  \mBbbP{}  \mmember{}  \mBbbU{}'


By

---

Latex:
Unfold  `pgeo-point`  0

---

Home Index