---

Step * of Lemma dp-perp_wf

∀[d:DualPlanePrimitives]. ∀[x,y:Vec].  ((x ⊥ y) ∈ ℙ)
BY
{ (Auto THEN (Assert d ∈ DualPlanePrimitives BY Trivial) THEN D 1 THEN Auto THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[d:DualPlanePrimitives].  \mforall{}[x,y:Vec].    ((x  \mbot{}  y)  \mmember{}  \mBbbP{})


By

---

Latex:
(Auto  THEN  (Assert  d  \mmember{}  DualPlanePrimitives  BY  Trivial)  THEN  D  1  THEN  Auto  THEN  ProveWfLemma)

---

Home Index