---

Step * of Lemma real-closed-interval-lattice_wf

No Annotations
∀[a,b:ℝ].  real-closed-interval-lattice(a;b) ∈ GeneralBoundedDistributiveLattice supposing a ≤ b
BY
{ (ProveWfLemma THEN Try ((MemTypeCD THEN EAuto 1)) THEN Try ((BLemma `req_inversion` THEN Complete (Auto)))) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
⊢ EquivRel({r:ℝ| (a ≤ r) ∧ (r ≤ b)} ;x,y.x = y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b:\mBbbR{}].    real-closed-interval-lattice(a;b)  \mmember{}  GeneralBoundedDistributiveLattice  supposing  a  \mleq{}  b


By

---

Latex:
(ProveWfLemma
  THEN  Try  ((MemTypeCD  THEN  EAuto  1))
  THEN  Try  ((BLemma  `req\_inversion`  THEN  Complete  (Auto))))

---

Home Index