theorem :: ALGGEO_1:40
for R being domRing
for n being non empty Ordinal
for V being non empty Algebraic_Set of n,R holds
( V is irreducible iff Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) )