X --> 0 is bag of X by Th39;
hence EmptyBag X is Element of Bags X by Def12; :: thesis: verum