---

Step * 1 1 of Lemma sdata-has-atom


1. d : SecurityData@i
2. a : Atom1@i
3. ¬(a ∈ sdata-atoms(d)) supposing a#d:SecurityData
4. a#d:SecurityData supposing ¬(a ∈ sdata-atoms(d))
5. ¬a#d:SecurityData@i
⊢ (a ∈ sdata-atoms(d))
BY
{ (SupposeNot THEN RepeatFor 2 (ThinTrivial) THEN Auto) }

---

Latex:

---

Latex:

1.  d  :  SecurityData@i
2.  a  :  Atom1@i
3.  \mneg{}(a  \mmember{}  sdata-atoms(d))  supposing  a\#d:SecurityData
4.  a\#d:SecurityData  supposing  \mneg{}(a  \mmember{}  sdata-atoms(d))
5.  \mneg{}a\#d:SecurityData@i
\mvdash{}  (a  \mmember{}  sdata-atoms(d))


By

---

Latex:
(SupposeNot  THEN  RepeatFor  2  (ThinTrivial)  THEN  Auto)

---

Home Index