let I be set ; :: thesis: for A, B, M being ManySortedSet of I st A c= M & B c= M holds
{A,B} is SubsetFamily of M
let A, B, M be ManySortedSet of I; :: thesis: ( A c= M & B c= M implies {A,B} is SubsetFamily of M )
assume ( A c= M & B c= M ) ; :: thesis: {A,B} is SubsetFamily of M
then ( {A} is SubsetFamily of M & {B} is SubsetFamily of M ) by Th7;
then {A} \/ {B} is SubsetFamily of M by Th3;
hence {A,B} is SubsetFamily of M by ENUMSET1:1; :: thesis: verum