Step
*
of Lemma
detach_msubset
∀s:DSet. ∀a,b:MSet{s}. ((↑(a ⊆b b))
⇒ (b = ((b - a) + a) ∈ MSet{s}))
BY
{ ((RepD) THENA Auto) }
1
1. s : DSet
2. a : MSet{s}
3. b : MSet{s}
4. ↑(a ⊆b b)
⊢ b = ((b - a) + a) ∈ MSet{s}
Latex:
Latex:
\mforall{}s:DSet. \mforall{}a,b:MSet\{s\}. ((\muparrow{}(a \msubseteq{}\msubb{} b)) {}\mRightarrow{} (b = ((b - a) + a)))
By
Latex:
((RepD) THENA Auto)
Home
Index