for S being set
for X, Y being ManySortedSet of S st X c= Y holds
Union (coprod X) c= Union (coprod Y)