take EmptyBag X ; :: thesis: EmptyBag X is zero
thus EmptyBag X is zero ; :: thesis: verum