---

Step * of Lemma mk-eu_wf

No Annotations
∀[self:GeometryPrimitives]. ∀[Sstab:∀a,b,c,d:Point.  SqStable(ab>cd)]. ∀[Lstab:∀a,b,c:Point.  SqStable(a # bc)].
∀[Sepor:∀a:Point. ∀b:{b:Point| a # b} . ∀c:Point.  (a # c ∨ b # c)]. ∀[nontriv:∃a:Point. (∃b:Point [a # b])].
∀[SS:∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} .  (∃x:Point [(Colinear(a;b;x) ∧ B(uxv))])].
∀[SC:∀c,d,a:Point. ∀b:{b:Point| b # a ∧ B(cbd)} .  (∃u:Point [(cu ≅ cd ∧ B(abu) ∧ (b # d ⇒ b # u))])].
∀[CC:∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:{d:Point| StrictOverlap(a;b;c;d)} .
       (∃u:Point [(ab ≅ au ∧ cd ≅ cu ∧ u leftof ac)])].
  (primitive=self
   Ssquashstable=Sstab
   Lorsquashstable=Lstab
   SepOr=Sepor
   nontriv=nontriv
   SS=SS
   SC=SC
   CC=CC ∈ EuclideanPlaneStructure)
BY
{ (Auto
   THEN Unfolds ``mk-eu euclidean-plane-structure`` 0
   THEN RepeatFor 7 ((RecordPlusTypeCD
                      THENL [ Id; (UnfoldGeoAbbreviations 0 THEN FoldGeoAbbreviations 0 THEN Try (Trivial))]
                     ))) }

1
1. self : GeometryPrimitives
2. Sstab : ∀a,b,c,d:Point.  SqStable(ab>cd)
3. Lstab : ∀a,b,c:Point.  SqStable(a # bc)
4. Sepor : ∀a:Point. ∀b:{b:Point| a # b} . ∀c:Point.  (a # c ∨ b # c)
5. nontriv : ∃a:Point. (∃b:Point [a # b])
6. SS : ∀a,b:Point. ∀u:{u:Point| u leftof ab} . ∀v:{v:Point| v leftof ba} .  (∃x:Point [(Colinear(a;b;x) ∧ B(uxv))])
7. SC : ∀c,d,a:Point. ∀b:{b:Point| b # a ∧ B(cbd)} .  (∃u:Point [(cu ≅ cd ∧ B(abu) ∧ (b # d ⇒ b # u))])
8. CC : ∀a,b:Point. ∀c:{c:Point| a # c} . ∀d:{d:Point| StrictOverlap(a;b;c;d)} .
          (∃u:Point [(ab ≅ au ∧ cd ≅ cu ∧ u leftof ac)])
⊢ self["Ssquashstable" := Sstab]["Lorsquashstable" := Lstab]["SepOr" := Sepor]["nontrivial" := nontriv]["SS" := SS]
  ["SS" := SS]["SC" := SC]["CC" := CC] ∈ GeometryPrimitives

---

Latex:

---

Latex:
No  Annotations
\mforall{}[self:GeometryPrimitives].  \mforall{}[Sstab:\mforall{}a,b,c,d:Point.    SqStable(ab>cd)].  \mforall{}[Lstab:\mforall{}a,b,c:Point.
                                                                                                                                                                  SqStable(a  \#  bc)].
\mforall{}[Sepor:\mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}c:Point.    (a  \#  c  \mvee{}  b  \#  c)].  \mforall{}[nontriv:\mexists{}a:Point
                                                                                                                                                              (\mexists{}b:Point  [a  \#  b])].
\mforall{}[SS:\mforall{}a,b:Point.  \mforall{}u:\{u:Point|  u  leftof  ab\}  .  \mforall{}v:\{v:Point|  v  leftof  ba\}  .
              (\mexists{}x:Point  [(Colinear(a;b;x)  \mwedge{}  B(uxv))])].  \mforall{}[SC:\mforall{}c,d,a:Point.  \mforall{}b:\{b:Point|  b  \#  a  \mwedge{}  B(cbd)\}  .
                                                                                                                (\mexists{}u:Point  [(cu  \mcong{}  cd
                                                                                                                                    \mwedge{}  B(abu)
                                                                                                                                    \mwedge{}  (b  \#  d  {}\mRightarrow{}  b  \#  u))])].
\mforall{}[CC:\mforall{}a,b:Point.  \mforall{}c:\{c:Point|  a  \#  c\}  .  \mforall{}d:\{d:Point|  StrictOverlap(a;b;c;d)\}  .
              (\mexists{}u:Point  [(ab  \mcong{}  au  \mwedge{}  cd  \mcong{}  cu  \mwedge{}  u  leftof  ac)])].
    (primitive=self
      Ssquashstable=Sstab
      Lorsquashstable=Lstab
      SepOr=Sepor
      nontriv=nontriv
      SS=SS
      SC=SC
      CC=CC  \mmember{}  EuclideanPlaneStructure)


By

---

Latex:
(Auto
  THEN  Unfolds  ``mk-eu  euclidean-plane-structure``  0
  THEN  RepeatFor  7  ((RecordPlusTypeCD
                                        THENL  [  Id
                                                    ;  (UnfoldGeoAbbreviations  0
                                                          THEN  FoldGeoAbbreviations  0
                                                          THEN  Try  (Trivial))]
                                      )))

---

Home Index