---

Step * 1 1 of Lemma pgeo-primitives_wf


"Point":Type
"Line":Type
"PS":self."Point" ⟶ self."Line" ⟶ ℙ ∈ 𝕌'
BY
{ (RecordWf THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RecordWf  THEN  Auto)

---

Home Index