theorem :: MBOOLEAN:17

for I being set
for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X (\/) Y))