theorem Th54: :: PBOOLE:54

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