thus X --> n is Multiset of X by Th27; :: thesis: verum