---

Step * of Lemma mk-pgeo_wf

∀[self:ProjGeomPrimitives]. ∀[ss:∀l:Line. ∀a:Point.  SqStable(a ≠ l)]. ∀[por:∀a:Point. ∀l:{l:Line| a ≠ l} . ∀m:Line.
                                                                               (a ≠ m ∨ m ≠ l)].
∀[lor:∀l:Line. ∀a:{a:Point| l ≠ a} . ∀b:Point.  (b ≠ l ∨ b ≠ a)].
∀[j:∀a,b:Point.  (a ≠ b ⇒ (∃l:Line. (a I l ∧ b I l)))]. ∀[m:∀l,m:Line.  (l ≠ m ⇒ (∃a:Point. (a I l ∧ a I m)))].
∀[p3:∀l:Line. ∃a,b,c:Point. (a I l ∧ b I l ∧ c I l ∧ a ≠ b ∧ b ≠ c ∧ c ≠ a)]. ∀[l3:∀a:Point
                                                                                     ∃l,m,n:Line
                                                                                      (a I l
                                                                                      ∧ a I m
                                                                                      ∧ a I n
                                                                                      ∧ l ≠ m
                                                                                      ∧ m ≠ n
                                                                                      ∧ n ≠ l)].
  (mk-pgeo(self; ss; por; lor; j; m; p3; l3) ∈ ProjectivePlaneStructure)
BY
{ ((Auto THEN Auto THEN Unfolds ``mk-pgeo projective-plane-structure`` 0)
   THEN RepeatFor 7 ((RecordPlusTypeCD
                      THENL [ Id
                            ; (UnfoldpGeoAbbreviations 0
                               THEN FoldpGeoAbbreviations 0
                               THEN (Trivial ORELSE (All (Folds ``pgeo-lpsep``) THEN Try (Trivial))))]
                     ))
   ) }

1
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

---

Latex:

---

Latex:
\mforall{}[self:ProjGeomPrimitives].  \mforall{}[ss:\mforall{}l:Line.  \mforall{}a:Point.    SqStable(a  \mneq{}  l)].  \mforall{}[por:\mforall{}a:Point.  \mforall{}l:\{l:Line| 
                                                                                                                                                                                      a  \mneq{}  l\}  .
                                                                                                                                                          \mforall{}m:Line.
                                                                                                                                                              (a  \mneq{}  m  \mvee{}  m  \mneq{}  l)].
\mforall{}[lor:\mforall{}l:Line.  \mforall{}a:\{a:Point|  l  \mneq{}  a\}  .  \mforall{}b:Point.    (b  \mneq{}  l  \mvee{}  b  \mneq{}  a)].  \mforall{}[j:\mforall{}a,b:Point.
                                                                                                                                              (a  \mneq{}  b
                                                                                                                                              {}\mRightarrow{}  (\mexists{}l:Line
                                                                                                                                                        (a  I  l  \mwedge{}  b  I  l)))].
\mforall{}[m:\mforall{}l,m:Line.    (l  \mneq{}  m  {}\mRightarrow{}  (\mexists{}a:Point.  (a  I  l  \mwedge{}  a  I  m)))].  \mforall{}[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)].  \mforall{}[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)].
    (mk-pgeo(self;  ss;  por;  lor;  j;  m;  p3;  l3)  \mmember{}  ProjectivePlaneStructure)


By

---

Latex:
((Auto  THEN  Auto  THEN  Unfolds  ``mk-pgeo  projective-plane-structure``  0)
  THEN  RepeatFor  7  ((RecordPlusTypeCD
                                        THENL  [  Id
                                                    ;  (UnfoldpGeoAbbreviations  0
                                                          THEN  FoldpGeoAbbreviations  0
                                                          THEN  (Trivial  ORELSE  (All  (Folds  ``pgeo-lpsep``)  THEN  Try  (Trivial))))]
                                      ))
  )

---

Home Index