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