---

Step * 1 of Lemma subtype_rel_bunion


1. A : Type@i'
2. B : Type@i'
3. A r B@i
 (A  B) r B
BY
{ (D 0 THEN Auto) }

1
1. A : Type@i'
2. B : Type@i'
3. A r B@i
4. x : A  B
 x  B



1.  A  :  Type@i'
2.  B  :  Type@i'
3.  A  \msubseteq{}r  B@i
\mvdash{}  (A  \mcup{}  B)  \msubseteq{}r  B


By

(D  0  THEN  Auto)



Home Index