let I be set ; :: thesis: for A, B, M being ManySortedSet of I st A c= M & B c= M holds
{A,B} is MSSubsetFamily of M
let A, B, M 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:10; :: thesis: verum