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