---

Step * of Lemma strong-subtype-b-union

∀[A,B:Type].  strong-subtype(A;A ⋃ B) ∧ strong-subtype(B;A ⋃ B) supposing ¬A ⋂ B
BY
{ ((UnivCD THENA Auto) THEN (Assert strong-subtype(A ⋂ B;Void) BY RepeatFor 2 ((D 0 THEN Auto))) THEN Auto) }

1
1. A : Type
2. B : Type
3. ¬A ⋂ B
4. strong-subtype(A ⋂ B;Void)
⊢ strong-subtype(A;A ⋃ B)

2
1. A : Type
2. B : Type
3. ¬A ⋂ B
4. strong-subtype(A ⋂ B;Void)
5. strong-subtype(A;A ⋃ B)
⊢ strong-subtype(B;A ⋃ B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    strong-subtype(A;A  \mcup{}  B)  \mwedge{}  strong-subtype(B;A  \mcup{}  B)  supposing  \mneg{}A  \mcap{}  B


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  strong-subtype(A  \mcap{}  B;Void)  BY
                          RepeatFor  2  ((D  0  THEN  Auto)))
  THEN  Auto)

---

Home Index