theorem Th1: :: MSAFREE4:1

for I being set
for f1, f2 being ManySortedSet of I st f1 c= f2 holds
Union f1 c= Union f2