---

Step * 1 of Lemma mk-pgeo_wf


1. self : ProjGeomPrimitives
2. ss : ∀l:Line. ∀a:Point.  SqStable(a ≠ l)
3. por : ∀a:Point. ∀l:{l:Line| a ≠ l} . ∀m:Line.  (a ≠ m ∨ m ≠ l)
4. lor : ∀l:Line. ∀a:{a:Point| l ≠ a} . ∀b:Point.  (b ≠ l ∨ b ≠ a)
5. j : ∀a,b:Point.  (a ≠ b ⇒ (∃l:Line. (a I l ∧ b I l)))
6. m : ∀l,m:Line.  (l ≠ m ⇒ (∃a:Point. (a I l ∧ a I m)))
7. p3 : ∀l:Line. ∃a,b,c:Point. (a I l ∧ b I l ∧ c I l ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a)
8. l3 : ∀a:Point. ∃l,m,n:Line. (a I l ∧ a I m ∧ a I n ∧ l ≠ m ∧ m ≠ n ∧ n ≠ l)
⊢ self["Ssquashstable" := ss]["PLSepOr" := por]["LPSepOr" := lor]["join" := j]["meet" := m]["three-points" := p3]
  ["three-lines" := l3] ∈ ProjGeomPrimitives
BY
{ (((Assert self ∈ ProjGeomPrimitives BY
           Auto)
    THEN (D 1 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.  self  :  ProjGeomPrimitives
2.  ss  :  \mforall{}l:Line.  \mforall{}a:Point.    SqStable(a  \mneq{}  l)
3.  por  :  \mforall{}a:Point.  \mforall{}l:\{l:Line|  a  \mneq{}  l\}  .  \mforall{}m:Line.    (a  \mneq{}  m  \mvee{}  m  \mneq{}  l)
4.  lor  :  \mforall{}l:Line.  \mforall{}a:\{a:Point|  l  \mneq{}  a\}  .  \mforall{}b:Point.    (b  \mneq{}  l  \mvee{}  b  \mneq{}  a)
5.  j  :  \mforall{}a,b:Point.    (a  \mneq{}  b  {}\mRightarrow{}  (\mexists{}l:Line.  (a  I  l  \mwedge{}  b  I  l)))
6.  m  :  \mforall{}l,m:Line.    (l  \mneq{}  m  {}\mRightarrow{}  (\mexists{}a:Point.  (a  I  l  \mwedge{}  a  I  m)))
7.  p3  :  \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)
8.  l3  :  \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{}  self["Ssquashstable"  :=  ss]["PLSepOr"  :=  por]["LPSepOr"  :=  lor]["join"  :=  j]["meet"  :=  m]
    ["three-points"  :=  p3]["three-lines"  :=  l3]  \mmember{}  ProjGeomPrimitives


By

---

Latex:
(((Assert  self  \mmember{}  ProjGeomPrimitives  BY
                  Auto)
    THEN  (D  1  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