theorem :: PRE_POLY:81

for X being set
for b being bag of X st support b = {} holds
b = EmptyBag X by Def7;