---

Step * of Lemma rmin-classical-cases

∀a,b:ℝ.  (¬¬((rmin(a;b) = a) ∨ (rmin(a;b) = b)))
BY
{ (Auto THEN (D 0 THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. ¬((rmin(a;b) = a) ∨ (rmin(a;b) = b))
⊢ False

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    (\mneg{}\mneg{}((rmin(a;b)  =  a)  \mvee{}  (rmin(a;b)  =  b)))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index