---

Step * of Lemma setmem_functionality_1

∀s,x1,x2:coSet{i:l}.  (seteq(x1;x2) ⇒ ((x1 ∈ s) ⇐⇒ (x2 ∈ s)))
BY
{ (UseWitness ⌜λs,x1,x2,eq. (setmemfunc(x1; s; x2; s) eq (seteqweaken(s) Ax))⌝⋅
   THEN Auto
   THEN InstLemma `seteqweaken_wf` [⌜s⌝;⌜s⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s,x1,x2:coSet\{i:l\}.    (seteq(x1;x2)  {}\mRightarrow{}  ((x1  \mmember{}  s)  \mLeftarrow{}{}\mRightarrow{}  (x2  \mmember{}  s)))


By

---

Latex:
(UseWitness  \mkleeneopen{}\mlambda{}s,x1,x2,eq.  (setmemfunc(x1;  s;  x2;  s)  eq  (seteqweaken(s)  Ax))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  InstLemma  `seteqweaken\_wf`  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index