:: deftheorem defines reducible ALGGEO_1:def 10 :
for R being domRing
for n being non empty Ordinal
for IT being Algebraic_Set of n,R holds
( IT is reducible iff ex V1, V2 being Algebraic_Set of n,R st
( IT = V1 \/ V2 & V1 c< IT & V2 c< IT ) );