:: deftheorem Def1 defines add-closed IDEAL_1:def 1 :
for L being non empty addLoopStr
for F being Subset of L holds
( F is add-closed iff for x, y being Element of L st x in F & y in F holds
x + y in F );