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