theorem :: ALGGEO_1:20

for R being domRing
for n being non empty Ordinal
for F being non empty Subset of (Ideals (Polynom-Ring (n,R))) holds Zero_ (union F) = meet { (Zero_ I) where I is Ideal of (Polynom-Ring (n,R)) : I in F }