:: deftheorem defines - REALALG1:def 6 :
for L being non empty addLoopStr
for S being Subset of L holds - S = { (- s) where s is Element of L : s in S } ;