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