consider b being natural-valued ManySortedSet of ;
b is real-valued ;
hence ex b₁ being ManySortedSet of st b₁ is real-valued ; :: thesis: verum