---

Step * of Lemma opposite-lattice_wf

∀[L:BoundedDistributiveLattice]. (opposite-lattice(L) ∈ BoundedDistributiveLattice)
BY
{ ((Auto THEN (Assert L ∈ DistributiveLattice BY Auto)) THEN D 1 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[L:BoundedDistributiveLattice].  (opposite-lattice(L)  \mmember{}  BoundedDistributiveLattice)


By

---

Latex:
((Auto  THEN  (Assert  L  \mmember{}  DistributiveLattice  BY  Auto))  THEN  D  1  THEN  ProveWfLemma)

---

Home Index