Step
*
1
of Lemma
not-atom-member-int
.....antecedent..... 
1. t : Atom
2. t ∈ ℤ@i
⊢ ↑isatom(t)
BY
{ (Thin (-1) THEN Auto) }
Latex:
Latex:
.....antecedent..... 
1.  t  :  Atom
2.  t  \mmember{}  \mBbbZ{}@i
\mvdash{}  \muparrow{}isatom(t)
By
Latex:
(Thin  (-1)  THEN  Auto)
Home
Index