:: deftheorem defines Ideal_ ALGGEO_1:def 9 :
for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds Ideal_ X = { f where f is Polynomial of n,R : X c= Zero_ f } ;