:: deftheorem defines Bag RING_5:def 1 :
for X being set
for S being finite Subset of X holds Bag S = (S,1) -bag ;