let I be set ; :: thesis: for A, M, B being ManySortedSet of I st A c= M & B c= M holds
{A,B} is MSSubsetFamily of M
let A, M, B be ManySortedSet of I; :: thesis: ( A c= M & B c= M implies {A,B} is MSSubsetFamily of M )
assume ( A c= M & B c= M ) ; :: thesis: {A,B} is MSSubsetFamily of M
then ( {A} is MSSubsetFamily of M & {B} is MSSubsetFamily of M ) by Th38;
then {A} \/ {B} is MSSubsetFamily of M by Th34;
hence {A,B} is MSSubsetFamily of M by PZFMISC1:11; :: thesis: verum