---

Step * of Lemma real-closed-interval-lattice_wf

∀[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)

2
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. EquivRel({r:ℝ| (a ≤ r) ∧ (r ≤ b)} ;x,y.x = y)
5. ∀[a1,b:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmin(a1;b) = rmin(b;a1))
6. ∀[a1,b:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmax(a1;b) = rmax(b;a1))
7. ∀[a1,b1,c:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmin(a1;rmin(b1;c)) = rmin(rmin(a1;b1);c))
8. ∀[a1,b1,c:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmax(a1;rmax(b1;c)) = rmax(rmax(a1;b1);c))
9. ∀[a1,b:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmax(a1;rmin(a1;b)) = a1)
10. ∀[a1,b:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmin(a1;rmax(a1;b)) = a1)
11. a1 : {r:ℝ| (a ≤ r) ∧ (r ≤ b)} 
⊢ rmin(a1;b) = a1

3
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. EquivRel({r:ℝ| (a ≤ r) ∧ (r ≤ b)} ;x,y.x = y)
5. ∀[a1,b:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmin(a1;b) = rmin(b;a1))
6. ∀[a1,b:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmax(a1;b) = rmax(b;a1))
7. ∀[a1,b1,c:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmin(a1;rmin(b1;c)) = rmin(rmin(a1;b1);c))
8. ∀[a1,b1,c:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmax(a1;rmax(b1;c)) = rmax(rmax(a1;b1);c))
9. ∀[a1,b:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmax(a1;rmin(a1;b)) = a1)
10. ∀[a1,b:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ].  (rmin(a1;rmax(a1;b)) = a1)
11. ∀[a:{r:ℝ| (a ≤ r) ∧ (r ≤ b)} ]. (rmin(a;b) = a)
12. a1 : {r:ℝ| (a ≤ r) ∧ (r ≤ b)} 
⊢ rmax(a1;a) = a1

---

Latex:

---

Latex:
\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