---

Step * of Lemma per-class-subtype-singleton

∀[T:Type]. ∀[a:T].  (per-class(T;a) ⊆r {x:T| x = a ∈ T} )
BY
{ (Auto THEN D 0 THEN Auto THEN D -1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a:T].    (per-class(T;a)  \msubseteq{}r  \{x:T|  x  =  a\}  )


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  D  -1  THEN  Auto)

---

Home Index