theorem :: MSSUBFAM:26

for I being set
for X, Y, Z being ManySortedSet of I st X is V39() & X c= [|Y,Z|] holds
ex A, B being ManySortedSet of I st
( A is V39() & A c= Y & B is V39() & B c= Z & X c= [|A,B|] )