let x be set ; :: thesis: ( x is Element of B implies x is ManySortedSet of )
assume x is Element of B ; :: thesis: x is ManySortedSet of
hence x is ManySortedSet of ; :: thesis: verum