:: deftheorem defines finitely_generated IDEAL_1:def 25 :
for L being non empty doubleLoopStr
for I being Ideal of L holds
( I is finitely_generated iff ex F being non empty finite Subset of L st I = F -Ideal );