theorem Th33: :: PRE_POLY:34

for X being set
for b, b1, b2 being natural-valued ManySortedSet of X st ( for x being object st x in X holds
b . x = (b1 . x) -' (b2 . x) ) holds
b = b1 -' b2