theorem :: IDEAL_1:97

for R being non empty doubleLoopStr st ( 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 ) ) holds
for a being sequence of R ex m being Element of NAT st a . (m + 1) in (rng (a | (m + 1))) -Ideal