theorem Th17: :: ALGGEO_1:17

for R being domRing
for n being non empty Ordinal
for S being non empty Subset of (Polynom-Ring (n,R)) holds Zero_ S = Zero_ (S -Ideal)