---

Step * of Lemma oob-subtype

∀[A1,B1,A2,B2:Type].  (one_or_both(A1;B1) ⊆r one_or_both(A2;B2)) supposing ((A1 ⊆r A2) and (B1 ⊆r B2))
BY
{ (Unfold `one_or_both` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A1,B1,A2,B2:Type].
    (one\_or\_both(A1;B1)  \msubseteq{}r  one\_or\_both(A2;B2))  supposing  ((A1  \msubseteq{}r  A2)  and  (B1  \msubseteq{}r  B2))


By

---

Latex:
(Unfold  `one\_or\_both`  0  THEN  Auto)

---

Home Index