---

Step * 1 1 1 of Lemma mk-complete-pgeo_wf


1. pg : ProjectivePlaneStructure
2. p : Point
⊢ pg["non-trivial" := <p, λx.x>] ∈ ProjectivePlaneStructure
BY
{ (D 1 THENA Auto) }

1
1. pg : self:ProjGeomPrimitives
        "Ssquashstable":∀l:Line. ∀a:Point.  SqStable(pgeo-plsep(self; a; l))
        "PLSepOr":∀a:Point. ∀l:{l:Line| pgeo-plsep(self; a; l)} . ∀m:Line.  (pgeo-plsep(self; a; m) ∨ m ≠ l)
        "LPSepOr":∀l:Line. ∀a:{a:Point| l ≠ a} . ∀b:Point.  (pgeo-plsep(self; b; l) ∨ b ≠ a)
        "join":∀a,b:Point.  (a ≠ b ⇒ (∃l:Line. (a I l ∧ b I l)))
        "meet":∀l,m:Line.  (l ≠ m ⇒ (∃a:Point. (a I l ∧ a I m)))
        "three-points":∀l:Line. ∃a,b,c:Point. (a I l ∧ b I l ∧ c I l ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a) ⋂ x:Atom
        ⟶ if x =a "three-lines"
           then ∀a:Point. ∃l,m,n:Line. (a I l ∧ a I m ∧ a I n ∧ l ≠ m ∧ m ≠ n ∧ n ≠ l)
           else Top
           fi 
2. pg ∈ ProjGeomPrimitives
3. p : Point
4. pg."Ssquashstable" ∈ ∀l:Line. ∀a:Point.  SqStable(pgeo-plsep(pg; a; l))
5. pg."PLSepOr" ∈ ∀a:Point. ∀l:{l:Line| pgeo-plsep(pg; a; l)} . ∀m:Line.  (pgeo-plsep(pg; a; m) ∨ m ≠ l)
6. pg."LPSepOr" ∈ ∀l:Line. ∀a:{a:Point| l ≠ a} . ∀b:Point.  (pgeo-plsep(pg; b; l) ∨ b ≠ a)
7. pg."join" ∈ ∀a,b:Point.  (a ≠ b ⇒ (∃l:Line. (a I l ∧ b I l)))
8. pg."meet" ∈ ∀l,m:Line.  (l ≠ m ⇒ (∃a:Point. (a I l ∧ a I m)))
9. pg."three-points" ∈ ∀l:Line. ∃a,b,c:Point. (a I l ∧ b I l ∧ c I l ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a)
10. pg."three-lines" ∈ ∀a:Point. ∃l,m,n:Line. (a I l ∧ a I m ∧ a I n ∧ l ≠ m ∧ m ≠ n ∧ n ≠ l)
⊢ pg["non-trivial" := <p, λx.x>] ∈ ProjectivePlaneStructure

---

Latex:

---

Latex:

1.  pg  :  ProjectivePlaneStructure
2.  p  :  Point
\mvdash{}  pg["non-trivial"  :=  <p,  \mlambda{}x.x>]  \mmember{}  ProjectivePlaneStructure


By

---

Latex:
(D  1  THENA  Auto)

---

Home Index