set r = the natural-valued finite-support ManySortedSet of X;
the natural-valued finite-support ManySortedSet of X = the natural-valued finite-support ManySortedSet of X ;
hence ex b₁ being ManySortedSet of X st
( b₁ is natural-valued & b₁ is finite-support ) ; :: thesis: verum