set b = the natural-valued ManySortedSet of X;
the natural-valued ManySortedSet of X is real-valued ;
hence ex b₁ being ManySortedSet of X st b₁ is real-valued ; :: thesis: verum