---

Step * 1 of Lemma per-class-base-singleton


1. T : Type
2. a : T
3. x : Base ⋂ {x:T| x = a ∈ T} 
4. x ∈ {x:T| x = a ∈ T} 
5. x ∈ Base
⊢ x ∈ per-class(T;a)
BY
{ (MemTypeHD (-2) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  a  :  T
3.  x  :  Base  \mcap{}  \{x:T|  x  =  a\} 
4.  x  \mmember{}  \{x:T|  x  =  a\} 
5.  x  \mmember{}  Base
\mvdash{}  x  \mmember{}  per-class(T;a)


By

---

Latex:
(MemTypeHD  (-2)  THEN  Auto)\mcdot{}

---

Home Index