---

Step * of Lemma real-interval-lattice_wf

∀[I:Interval]. (real-interval-lattice(I) ∈ DistributiveLattice)
BY
{ (ProveWfLemma
   THEN Try ((MemTypeCD THEN EAuto 1))
   THEN Try ((BLemma `implies-equal-real` THEN Auto THEN RepUR ``rmin rmax`` 0 THEN Auto))
   THEN Try (((BLemma `rmin-i-member` ORELSE BLemma `rmax-i-member`) THEN EAuto 1))) }

---

Latex:

---

Latex:
\mforall{}[I:Interval].  (real-interval-lattice(I)  \mmember{}  DistributiveLattice)


By

---

Latex:
(ProveWfLemma
  THEN  Try  ((MemTypeCD  THEN  EAuto  1))
  THEN  Try  ((BLemma  `implies-equal-real`  THEN  Auto  THEN  RepUR  ``rmin  rmax``  0  THEN  Auto))
  THEN  Try  (((BLemma  `rmin-i-member`  ORELSE  BLemma  `rmax-i-member`)  THEN  EAuto  1)))

---

Home Index