---

Step * of Lemma rrel*_functionality

∀[R:ℝ ⟶ ℝ ⟶ ℙ]
  ((∀x1,x2,y1,y2:ℝ.  ((x1 = x2) ⇒ (y1 = y2) ⇒ (R x1 y1 ⇐⇒ R x2 y2)))
  ⇒ (∀x1,x2,y1,y2:ℝ*.  (x1 = x2 ⇒ y1 = y2 ⇒ (R*(x1,y1) ⇐⇒ R*(x2,y2)))))
BY
{ (Auto
   THEN D -3
   THEN D -2
   THEN D -1
   THEN D 0 With ⌜imax(n;imax(n1;n2))⌝ 
   THEN Auto
   THEN ∀h:hyp. (InstHyp [⌜m⌝] h⋅ THENA Complete (Auto)) 
   THEN FHyp 2 [-1;-2;-3]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[R:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}x1,x2,y1,y2:\mBbbR{}.    ((x1  =  x2)  {}\mRightarrow{}  (y1  =  y2)  {}\mRightarrow{}  (R  x1  y1  \mLeftarrow{}{}\mRightarrow{}  R  x2  y2)))
    {}\mRightarrow{}  (\mforall{}x1,x2,y1,y2:\mBbbR{}*.    (x1  =  x2  {}\mRightarrow{}  y1  =  y2  {}\mRightarrow{}  (R*(x1,y1)  \mLeftarrow{}{}\mRightarrow{}  R*(x2,y2)))))


By

---

Latex:
(Auto
  THEN  D  -3
  THEN  D  -2
  THEN  D  -1
  THEN  D  0  With  \mkleeneopen{}imax(n;imax(n1;n2))\mkleeneclose{} 
  THEN  Auto
  THEN  \mforall{}h:hyp.  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto)) 
  THEN  FHyp  2  [-1;-2;-3]
  THEN  Auto)

---

Home Index