---

Step * of Lemma rmin_functionality

∀[x1,x2,y1,y2:ℝ].  (rmin(x1;y1) = rmin(x2;y2)) supposing ((x1 = x2) and (y1 = y2))
BY
{ (Auto THEN All (RWO "req-iff-bdd-diff" )⋅ THEN Auto THEN RWO "-1 -2" 0 THEN Auto THEN RelRST THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}[x1,x2,y1,y2:\mBbbR{}].    (rmin(x1;y1)  =  rmin(x2;y2))  supposing  ((x1  =  x2)  and  (y1  =  y2))


By

---

Latex:
(Auto
  THEN  All
  (RWO  "req-iff-bdd-diff"  )\mcdot{}
  THEN  Auto
  THEN  RWO  "-1  -2"  0
  THEN  Auto
  THEN  RelRST
  THEN  Auto)\mcdot{}

---

Home Index