---

Step * of Lemma least-upper-bound-unique

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀[a,b,c,d:T].
    (c = d ∈ T) supposing (least-upper-bound(T;x,y.R[x;y];a;b;c) and least-upper-bound(T;x,y.R[x;y];a;b;d)) 
  supposing Order(T;x,y.R[x;y])
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}[a,b,c,d:T].
        (c  =  d)  supposing 
              (least-upper-bound(T;x,y.R[x;y];a;b;c)  and 
              least-upper-bound(T;x,y.R[x;y];a;b;d)) 
    supposing  Order(T;x,y.R[x;y])


By

---

Latex:
Auto

---

Home Index