:: deftheorem defines Ideals RING_2:def 3 :
for R being Ring holds Ideals R = { I where I is Ideal of R : verum } ;