---

Step * of Lemma subset-comp-structure

No Annotations
∀[X,Y:j⊢]. ∀[T:{Y ⊢ _}].  Y ⊢ Compositon(T) ⊆r X ⊢ Compositon(T) supposing sub_cubical_set{j:l}(X; Y)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN RenameVar `cT' (-1)
   THEN D -1
   THEN Assert ⌜cT ∈ composition-function{j:l,i:l}(X;T)⌝⋅) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:j\mvdash{}].  \mforall{}[T:\{Y  \mvdash{}  \_\}].
    Y  \mvdash{}  Compositon(T)  \msubseteq{}r  X  \mvdash{}  Compositon(T)  supposing  sub\_cubical\_set\{j:l\}(X;  Y)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  RenameVar  `cT'  (-1)
  THEN  D  -1
  THEN  Assert  \mkleeneopen{}cT  \mmember{}  composition-function\{j:l,i:l\}(X;T)\mkleeneclose{}\mcdot{})

---

Home Index