---

Step * of Lemma real-weak-Markov

No Annotations
∀x,y:ℝ.  x ≠ y supposing ∀z:ℝ. ((¬(z = x)) ∨ (¬(z = y)))
BY
{ (Auto THEN (BLemma `rneq-if-rabs` THENA Auto) THEN BLemma  `pseudo-positive-is-positive` THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. ∀z:ℝ. ((¬(z = x)) ∨ (¬(z = y)))
⊢ pseudo-positive(|x - y|)

---

Latex:

---

Latex:
No  Annotations
\mforall{}x,y:\mBbbR{}.    x  \mneq{}  y  supposing  \mforall{}z:\mBbbR{}.  ((\mneg{}(z  =  x))  \mvee{}  (\mneg{}(z  =  y)))


By

---

Latex:
(Auto  THEN  (BLemma  `rneq-if-rabs`  THENA  Auto)  THEN  BLemma    `pseudo-positive-is-positive`  THEN  Auto)

---

Home Index