theorem Th3: :: INT_7:3

for X being set
for p, q being ManySortedSet of X st p | (support p) = q | (support q) holds
p = q