theorem :: MSSUBFAM:27

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