theorem Th53: :: PBOOLE:53

for I being set
for X, Y, Z being ManySortedSet of I st X c= Y holds
X (\) Z c= Y (\) Z