---

Step * of Lemma mk-dp_wf

∀[self:DualPlanePrimitives]. ∀[sqs:∀x,y:Vec.  SqStable((x # y))]. ∀[st:∀x,y:Vec.  Stable{(x ⊥ y)}].
∀[sor:∀x:Vec. ∀y:{y:Vec| (x # y)} . ∀z:Vec.  ((z # x) ∨ (z # y))]. ∀[crs:∀a:Vec. ∀b:{b:Vec| (a # b)} .
                                                                          (∃c:Vec [((a ⊥ c) ∧ (b ⊥ c))])].
∀[nt:∀a:Vec. (∃c:Vec [((a ⊥ c) ∧ (a # c))])].
  (mk-dp(self;sqs;st;sor;crs;nt) ∈ DualPlaneStructure)
BY
{ (Auto THEN Unfolds ``mk-dp dual-plane-structure`` 0) }

1
1. self : DualPlanePrimitives
2. sqs : ∀x,y:Vec.  SqStable((x # y))
3. st : ∀x,y:Vec.  Stable{(x ⊥ y)}
4. sor : ∀x:Vec. ∀y:{y:Vec| (x # y)} . ∀z:Vec.  ((z # x) ∨ (z # y))
5. crs : ∀a:Vec. ∀b:{b:Vec| (a # b)} .  (∃c:Vec [((a ⊥ c) ∧ (b ⊥ c))])
6. nt : ∀a:Vec. (∃c:Vec [((a ⊥ c) ∧ (a # c))])
⊢ self["Ssquashstable" := sqs]["Pstable" := st]["SepOr" := sor]["cross" := crs]["nontrivial" := nt]
  ∈ DualPlanePrimitives
  "Ssquashstable":∀x,y:Vec.  SqStable((x # y))
  "Pstable":∀x,y:Vec.  Stable{(x ⊥ y)}
  "SepOr":∀x:Vec. ∀y:{y:Vec| (x # y)} . ∀z:Vec.  ((z # x) ∨ (z # y))
  "cross":∀a:Vec. ∀b:{b:Vec| (a # b)} .  (∃c:Vec [((a ⊥ c) ∧ (b ⊥ c))])
  "nontrivial":∀a:Vec. (∃c:Vec [((a ⊥ c) ∧ (a # c))])

---

Latex:

---

Latex:
\mforall{}[self:DualPlanePrimitives].  \mforall{}[sqs:\mforall{}x,y:Vec.    SqStable((x  \#  y))].  \mforall{}[st:\mforall{}x,y:Vec.    Stable\{(x  \mbot{}  y)\}].
\mforall{}[sor:\mforall{}x:Vec.  \mforall{}y:\{y:Vec|  (x  \#  y)\}  .  \mforall{}z:Vec.    ((z  \#  x)  \mvee{}  (z  \#  y))].  \mforall{}[crs:\mforall{}a:Vec.  \mforall{}b:\{b:Vec|  (a  \#  b)\}\000C  .
                                                                                                                                                    (\mexists{}c:Vec  [((a  \mbot{}  c)
                                                                                                                                                                    \mwedge{}  (b  \mbot{}  c))])].
\mforall{}[nt:\mforall{}a:Vec.  (\mexists{}c:Vec  [((a  \mbot{}  c)  \mwedge{}  (a  \#  c))])].
    (mk-dp(self;sqs;st;sor;crs;nt)  \mmember{}  DualPlaneStructure)


By

---

Latex:
(Auto  THEN  Unfolds  ``mk-dp  dual-plane-structure``  0)

---

Home Index