:: deftheorem defines principal IDEAL_1:def 27 :
for L being non empty doubleLoopStr
for I being Ideal of L holds
( I is principal iff ex e being Element of L st I = {e} -Ideal );