:: deftheorem defines PID IDEAL_1:def 28 :
for L being non empty doubleLoopStr holds
( L is PID iff for I being Ideal of L holds I is principal );