---

Step * of Lemma t-sqle-base

∀[T:Type]. ∀a,b:T.  (t-sqle(T;a;b) ⇒ (a ≤ b)) supposing T ⊆r Base
BY
{ ((UnivCD THENA Auto)
   THEN D -1
   THEN SqUnhide
   THEN ExRepD
   THEN ((InstLemma `per-class-base` [⌜T⌝;⌜a⌝;⌜a'⌝]⋅ THENA Auto) THEN RWO "-1<" 0)
   THEN (InstLemma `per-class-base` [⌜T⌝;⌜b⌝;⌜b'⌝]⋅ THENA Auto)
   THEN RWO "-1<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}a,b:T.    (t-sqle(T;a;b)  {}\mRightarrow{}  (a  \mleq{}  b))  supposing  T  \msubseteq{}r  Base


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  -1
  THEN  SqUnhide
  THEN  ExRepD
  THEN  ((InstLemma  `per-class-base`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RWO  "-1<"  0)
  THEN  (InstLemma  `per-class-base`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index