---

Step * 2 of Lemma basic-pgeo-axioms-imply


1. g : ProjectivePlaneStructure@i'
2. BasicProjectiveGeometryAxioms(g)
3. ∀a:Point. a ≡ a
4. l : Line@i
⊢ l ≡ l
BY
{ ((StableCases ⌜l ≡ l⌝⋅ THEN Auto) THEN (D 0 THENA Auto)) }

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

---

Latex:

---

Latex:

1.  g  :  ProjectivePlaneStructure@i'
2.  BasicProjectiveGeometryAxioms(g)
3.  \mforall{}a:Point.  a  \mequiv{}  a
4.  l  :  Line@i
\mvdash{}  l  \mequiv{}  l


By

---

Latex:
((StableCases  \mkleeneopen{}l  \mequiv{}  l\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index