theorem Th118: :: ABCMIZ_1:118

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