---

Step * of Lemma mk-eu_wf2

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 ∈ EuclideanPlane 
  supposing BasicGeometryAxioms(self)
BY
{ (Intros
   THEN (MemTypeCD THENW Auto)
   THEN Try ((BLemma `mk-eu_wf` THEN Trivial))
   THEN ParallelLast
   THEN NthHypSq (-1)
   THEN RepUR ``basic-geo-axioms mk-eu geo-lsep`` 0
   THEN UnfoldGeoAbbreviations 0
   THEN SqEqCD) }

---

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{}  EuclideanPlane 
    supposing  BasicGeometryAxioms(self)


By

---

Latex:
(Intros
  THEN  (MemTypeCD  THENW  Auto)
  THEN  Try  ((BLemma  `mk-eu\_wf`  THEN  Trivial))
  THEN  ParallelLast
  THEN  NthHypSq  (-1)
  THEN  RepUR  ``basic-geo-axioms  mk-eu  geo-lsep``  0
  THEN  UnfoldGeoAbbreviations  0
  THEN  SqEqCD)

---

Home Index