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