---

Step * of Lemma fset_properties

∀s:DSet. ∀a:FiniteSet{s}.  {∀x:|s|. ((x #∈ a) ≤ 1)}
BY
{ (Unfold `guard` 0 THEN ((RepD THENM BasicAbSetHD 2) THENA Auto)) }

1
1. s : DSet@i'
2. a : MSet{s}@i
3. [%1] : ∀x:|s|. ((x #∈ a) ≤ 1)@i
4. x : |s|@i
⊢ (x #∈ a) ≤ 1

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:FiniteSet\{s\}.    \{\mforall{}x:|s|.  ((x  \#\mmember{}  a)  \mleq{}  1)\}


By

---

Latex:
(Unfold  `guard`  0  THEN  ((RepD  THENM  BasicAbSetHD  2)  THENA  Auto))

---

Home Index