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