let I be set ; :: thesis: for A, M being ManySortedSet of I st A c= M holds
{A} is SubsetFamily of M
let A, M be ManySortedSet of I; :: thesis: ( A c= M implies {A} is SubsetFamily of M )
assume A c= M ; :: thesis: {A} is SubsetFamily of M
then A is ManySortedSubset of M by PBOOLE:def 18;
then A in Bool M by Def1;
hence {A} is SubsetFamily of M by ZFMISC_1:31; :: thesis: verum