---

Step * of Lemma inf-unique

∀[A:Set(ℝ)]. ∀[b,c:ℝ].  (inf(A) = b ⇒ inf(A) = c ⇒ (b = c))
BY
{ (Auto THEN (Assert ⌜(b ≤ c) ∧ (c ≤ b)⌝⋅ THENM EAuto 1) THEN D 0) }

1
1. A : Set(ℝ)
2. b : ℝ
3. c : ℝ
4. inf(A) = b
5. inf(A) = c
⊢ b ≤ c

2
1. A : Set(ℝ)
2. b : ℝ
3. c : ℝ
4. inf(A) = b
5. inf(A) = c
⊢ c ≤ b

---

Latex:

---

Latex:
\mforall{}[A:Set(\mBbbR{})].  \mforall{}[b,c:\mBbbR{}].    (inf(A)  =  b  {}\mRightarrow{}  inf(A)  =  c  {}\mRightarrow{}  (b  =  c))


By

---

Latex:
(Auto  THEN  (Assert  \mkleeneopen{}(b  \mleq{}  c)  \mwedge{}  (c  \mleq{}  b)\mkleeneclose{}\mcdot{}  THENM  EAuto  1)  THEN  D  0)

---

Home Index