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