:: deftheorem defines trivial IDEAL_1:def 4 :
for R being non empty add-cancelable right_zeroed distributive left_zeroed doubleLoopStr
for I being Ideal of R holds
( I is trivial iff I = {(0. R)} );