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