---

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


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
BY
{ Unfolds ``projective-plane-structure`` 0 }

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>] ∈ 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)
  "three-lines":∀a:Point. ∃l,m,n:Line. (a I l ∧ a I m ∧ a I n ∧ l ≠ m ∧ m ≠ n ∧ n ≠ l)

---

Latex:

---

Latex:

1.  pg  :  self:ProjGeomPrimitives
                "Ssquashstable":\mforall{}l:Line.  \mforall{}a:Point.    SqStable(pgeo-plsep(self;  a;  l))
                "PLSepOr":\mforall{}a:Point.  \mforall{}l:\{l:Line|  pgeo-plsep(self;  a;  l)\}  .  \mforall{}m:Line.
                                        (pgeo-plsep(self;  a;  m)  \mvee{}  m  \mneq{}  l)
                "LPSepOr":\mforall{}l:Line.  \mforall{}a:\{a:Point|  l  \mneq{}  a\}  .  \mforall{}b:Point.    (pgeo-plsep(self;  b;  l)  \mvee{}  b  \mneq{}  a)
                "join":\mforall{}a,b:Point.    (a  \mneq{}  b  {}\mRightarrow{}  (\mexists{}l:Line.  (a  I  l  \mwedge{}  b  I  l)))
                "meet":\mforall{}l,m:Line.    (l  \mneq{}  m  {}\mRightarrow{}  (\mexists{}a:Point.  (a  I  l  \mwedge{}  a  I  m)))
                "three-points":\mforall{}l:Line.  \mexists{}a,b,c:Point.  (a  I  l  \mwedge{}  b  I  l  \mwedge{}  c  I  l  \mwedge{}  a  \mneq{}  b  \mwedge{}  b  \mneq{}  c  \mwedge{}  c  \mneq{}  a)
                \mcap{}  x:Atom  {}\mrightarrow{}  if  x  =a  "three-lines"
                                        then  \mforall{}a:Point.  \mexists{}l,m,n:Line.  (a  I  l  \mwedge{}  a  I  m  \mwedge{}  a  I  n  \mwedge{}  l  \mneq{}  m  \mwedge{}  m  \mneq{}  n  \mwedge{}  n  \mneq{}  l)
                                        else  Top
                                        fi 
2.  pg  \mmember{}  ProjGeomPrimitives
3.  p  :  Point
4.  pg."Ssquashstable"  \mmember{}  \mforall{}l:Line.  \mforall{}a:Point.    SqStable(pgeo-plsep(pg;  a;  l))
5.  pg."PLSepOr"  \mmember{}  \mforall{}a:Point.  \mforall{}l:\{l:Line|  pgeo-plsep(pg;  a;  l)\}  .  \mforall{}m:Line.
                                        (pgeo-plsep(pg;  a;  m)  \mvee{}  m  \mneq{}  l)
6.  pg."LPSepOr"  \mmember{}  \mforall{}l:Line.  \mforall{}a:\{a:Point|  l  \mneq{}  a\}  .  \mforall{}b:Point.    (pgeo-plsep(pg;  b;  l)  \mvee{}  b  \mneq{}  a)
7.  pg."join"  \mmember{}  \mforall{}a,b:Point.    (a  \mneq{}  b  {}\mRightarrow{}  (\mexists{}l:Line.  (a  I  l  \mwedge{}  b  I  l)))
8.  pg."meet"  \mmember{}  \mforall{}l,m:Line.    (l  \mneq{}  m  {}\mRightarrow{}  (\mexists{}a:Point.  (a  I  l  \mwedge{}  a  I  m)))
9.  pg."three-points"  \mmember{}  \mforall{}l:Line.  \mexists{}a,b,c:Point.  (a  I  l  \mwedge{}  b  I  l  \mwedge{}  c  I  l  \mwedge{}  a  \mneq{}  b  \mwedge{}  b  \mneq{}  c  \mwedge{}  c  \mneq{}  a)
10.  pg."three-lines"  \mmember{}  \mforall{}a:Point.  \mexists{}l,m,n:Line.  (a  I  l  \mwedge{}  a  I  m  \mwedge{}  a  I  n  \mwedge{}  l  \mneq{}  m  \mwedge{}  m  \mneq{}  n  \mwedge{}  n  \mneq{}  l)
\mvdash{}  pg["non-trivial"  :=  <p,  \mlambda{}x.x>]  \mmember{}  ProjectivePlaneStructure


By

---

Latex:
Unfolds  ``projective-plane-structure``  0

---

Home Index