---

Step * of Lemma rmin-com

∀[x,y:ℝ].  (rmin(x;y) = rmin(y;x))
BY
{ (Auto⋅
   THEN (BLemma `req_weakening` THEN Auto)
   THEN (Assert rmin(x;y) ∈ ℝ BY
               Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN (Ext THENM RepUR ``rmin`` 0)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (rmin(x;y)  =  rmin(y;x))


By

---

Latex:
(Auto\mcdot{}
  THEN  (BLemma  `req\_weakening`  THEN  Auto)
  THEN  (Assert  rmin(x;y)  \mmember{}  \mBbbR{}  BY
                          Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (Ext  THENM  RepUR  ``rmin``  0)
  THEN  Auto)

---

Home Index