---

Step * of Lemma basic-pgeo-axioms-imply

∀g:ProjectivePlaneStructure. (BasicProjectiveGeometryAxioms(g) ⇒ ((∀a:Point. a ≡ a) ∧ (∀l:Line. l ≡ l)))
BY
{ Auto }

1
1. g : ProjectivePlaneStructure@i'
2. BasicProjectiveGeometryAxioms(g)
3. a : Point@i
⊢ a ≡ a

2
1. g : ProjectivePlaneStructure@i'
2. BasicProjectiveGeometryAxioms(g)
3. ∀a:Point. a ≡ a
4. l : Line@i
⊢ l ≡ l

---

Latex:

---

Latex:
\mforall{}g:ProjectivePlaneStructure
    (BasicProjectiveGeometryAxioms(g)  {}\mRightarrow{}  ((\mforall{}a:Point.  a  \mequiv{}  a)  \mwedge{}  (\mforall{}l:Line.  l  \mequiv{}  l)))


By

---

Latex:
Auto

---

Home Index