---

Step * 1 1 1 of Lemma sv-classrel


1. Info : Type
2. A : Type
3. X : EClass(A)
4. es : EO+(Info)@i'
5. e : E@i
6. v : A@i
7. ∀e:E. (#(X es e) ≤ 1)@i'
8. #(X es e) ≤ 1
⊢ v ↓∈ X es e ⇐⇒ (↑(#(X es e) =z 1)) ∧ (v = only(X es e) ∈ A)
BY
{ (MoveToConcl (-1) THEN (GenConcl ⌈(X es e) = b ∈ bag(A)⌉⋅ THENA Auto) THEN All Thin) }

1
1. A : Type
2. v : A@i
3. b : bag(A)@i
⊢ (#(b) ≤ 1) ⇒ (v ↓∈ b ⇐⇒ (↑(#(b) =z 1)) ∧ (v = only(b) ∈ A))

---

Latex:



1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)
4.  es  :  EO+(Info)@i'
5.  e  :  E@i
6.  v  :  A@i
7.  \mforall{}e:E.  (\#(X  es  e)  \mleq{}  1)@i'
8.  \#(X  es  e)  \mleq{}  1
\mvdash{}  v  \mdownarrow{}\mmember{}  X  es  e  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(\#(X  es  e)  =\msubz{}  1))  \mwedge{}  (v  =  only(X  es  e))


By

(MoveToConcl  (-1)  THEN  (GenConcl  \mkleeneopen{}(X  es  e)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)

---

Home Index