---

Step * 1 1 1 1 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. p : Point
3. self : ProjGeomPrimitives@i'
⊢ self["non-trivial" := <p, λx.x>] ∈ ProjGeomPrimitives
BY
{ (((Assert self ∈ ProjGeomPrimitives BY
           Auto)
    THEN (D 3 THENA Auto)
    THEN Unfold `pgeo-primitives` 0
    THEN RepeatFor 3 ((RecordPlusTypeCD
                       THENL [ Id
                             ; (UnfoldpGeoAbbreviations 0
                                THEN FoldpGeoAbbreviations 0
                                THEN (Trivial ORELSE (MemCD THEN Trivial)))]
                      )))
   THEN RepUR ``record record-update`` 0
   THEN Auto) }

---

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.  p  :  Point
3.  self  :  ProjGeomPrimitives@i'
\mvdash{}  self["non-trivial"  :=  <p,  \mlambda{}x.x>]  \mmember{}  ProjGeomPrimitives


By

---

Latex:
(((Assert  self  \mmember{}  ProjGeomPrimitives  BY
                  Auto)
    THEN  (D  3  THENA  Auto)
    THEN  Unfold  `pgeo-primitives`  0
    THEN  RepeatFor  3  ((RecordPlusTypeCD
                                          THENL  [  Id
                                                      ;  (UnfoldpGeoAbbreviations  0
                                                            THEN  FoldpGeoAbbreviations  0
                                                            THEN  (Trivial  ORELSE  (MemCD  THEN  Trivial)))]
                                        )))
  THEN  RepUR  ``record  record-update``  0
  THEN  Auto)

---

Home Index