---

Step * of Lemma composition-function-subset

No Annotations
∀[Y,X:j⊢].
  ∀[B:{X ⊢ _}]. (composition-function{j:l,i:l}(X;B) ⊆r composition-function{j:l,i:l}(Y;B)) 
  supposing sub_cubical_set{j:l}(Y; X)
BY
{ (Intros THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. Y : CubicalSet{j}
2. X : CubicalSet{j}
3. sub_cubical_set{j:l}(Y; X)
4. B : {X ⊢ _}
5. x : composition-function{j:l,i:l}(X;B)
⊢ x ∈ composition-function{j:l,i:l}(Y;B)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Y,X:j\mvdash{}].
    \mforall{}[B:\{X  \mvdash{}  \_\}].  (composition-function\{j:l,i:l\}(X;B)  \msubseteq{}r  composition-function\{j:l,i:l\}(Y;B)) 
    supposing  sub\_cubical\_set\{j:l\}(Y;  X)


By

---

Latex:
(Intros  THEN  (D  0  THENA  Auto))

---

Home Index