:: deftheorem defines are_disjoint GROEB_2:def 3 :
for X being set
for b1, b2 being bag of X holds
( b1,b2 are_disjoint iff for i being object holds
( b1 . i = 0 or b2 . i = 0 ) );