---

Step * of Lemma t-sqle-subtype

∀[A,B:Type].  ∀[a,b:A].  (t-sqle(A;a;b) ⇒ t-sqle(B;a;b)) supposing A ⊆r B
BY
{ (Auto THEN RepeatFor 4 (ParallelLast)) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelLast))

---

Home Index