---

Step * of Lemma rmax-com

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

---

Latex:

---

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


By

---

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

---

Home Index