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