:: deftheorem defines add| IDEAL_1:def 5 :
for R being non empty addLoopStr
for I being non empty add-closed Subset of R holds add| (I,R) = the addF of R || I;