---

Step * 4 1 of Lemma fset_of_mset_mem


1. s : DSet
2. c : |s|
3. ys : MSet{s}
4. ys' : MSet{s}
5. c ∈b fset_of_mset(s;ys) = c ∈b ys
6. c ∈b fset_of_mset(s;ys') = c ∈b ys'
⊢ c ∈b fset_of_mset(s;ys) ⋃ fset_of_mset(s;ys') = (c ∈b ys) ∨b(c ∈b ys')
BY
{ ((RewriteWith [5;6] ``fset_mem_union`` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  c  :  |s|
3.  ys  :  MSet\{s\}
4.  ys'  :  MSet\{s\}
5.  c  \mmember{}\msubb{}  fset\_of\_mset(s;ys)  =  c  \mmember{}\msubb{}  ys
6.  c  \mmember{}\msubb{}  fset\_of\_mset(s;ys')  =  c  \mmember{}\msubb{}  ys'
\mvdash{}  c  \mmember{}\msubb{}  fset\_of\_mset(s;ys)  \mcup{}  fset\_of\_mset(s;ys')  =  (c  \mmember{}\msubb{}  ys)  \mvee{}\msubb{}(c  \mmember{}\msubb{}  ys')


By

---

Latex:
((RewriteWith  [5;6]  ``fset\_mem\_union``  0)  THEN  Auto)

---

Home Index