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