---

Step * of Lemma subtype_rel_isect2

∀[A,B,C:Type].  uiff(A ⊆r B ⋂ C;(A ⊆r B) ∧ (A ⊆r C))
BY
{ (Unfold `isect2` 0 THEN (UnivCD THENA Auto) THEN (RWO "subtype_rel_isect" 0 THEN Auto)⋅) }

1
1. A : Type
2. B : Type
3. C : Type
4. ∀[b:𝔹]. (A ⊆r if b then B else C fi )
⊢ A ⊆r B

2
1. A : Type
2. B : Type
3. C : Type
4. ∀[b:𝔹]. (A ⊆r if b then B else C fi )
⊢ A ⊆r C

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].    uiff(A  \msubseteq{}r  B  \mcap{}  C;(A  \msubseteq{}r  B)  \mwedge{}  (A  \msubseteq{}r  C))


By

---

Latex:
(Unfold  `isect2`  0  THEN  (UnivCD  THENA  Auto)  THEN  (RWO  "subtype\_rel\_isect"  0  THEN  Auto)\mcdot{})

---

Home Index