consider f being ManySortedSet of , g being ManySortedSet of ;
take [f,g] ; :: thesis: ex f being ManySortedSet of ex g being ManySortedSet of st [f,g] = [f,g]
take f ; :: thesis: ex g being ManySortedSet of st [f,g] = [f,g]
take g ; :: thesis: [f,g] = [f,g]
thus [f,g] = [f,g] ; :: thesis: verum