let V be non empty addLoopStr ; :: thesis: [#] V is add-closed
for v, u being Element of V st v in [#] V & u in [#] V holds
v + u in [#] V ;
hence [#] V is add-closed by IDEAL_1:def 1; :: thesis: verum