theorem :: IDEAL_1:96

for R being non empty add-cancelable add-associative right_zeroed well-unital distributive associative left_zeroed Noetherian doubleLoopStr
for B being non empty Subset of R ex C being non empty finite Subset of R st
( C c= B & C -Ideal = B -Ideal )