:: deftheorem Def7 defines algebraic_set_from_ideal ALGGEO_1:def 6 :
for R being domRing
for n being non empty Ordinal
for IT being Subset of (Funcs (n,([#] R))) holds
( IT is algebraic_set_from_ideal iff ex I being Ideal of (Polynom-Ring (n,R)) st IT = Zero_ I );