1. r : Rng
2. a : |r|
⊢ (a)r ∈ Ideal(r){i}
{ TACTIC:MemTypeCD }
⊢ (a)r ∈ |r| ⟶ ℙ
.....set predicate.....
⊢ (a)r Ideal of r
.....wf.....
3. p : |r| ⟶ ℙ
⊢ istype(p Ideal of r)