let b be Element of B; :: thesis: b is bag of X
thus b is bag of X by Def14; :: thesis: verum