---

Step * of Lemma qabs-difference-symmetry

∀[x,y:ℚ].  (|x - y| = |y - x| ∈ ℚ)
BY
{ ((Auto THEN RW (AddrC [2] (LemmaC `qabs-qminus` ) ) 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbQ{}].    (|x  -  y|  =  |y  -  x|)


By

---

Latex:
((Auto  THEN  RW  (AddrC  [2]  (LemmaC  `qabs-qminus`  )  )  0)  THEN  Auto)

---

Home Index