let I be set ; :: thesis: for A, M being ManySortedSet of I st A c= M holds
{A} is MSSubsetFamily of M
let A, M be ManySortedSet of I; :: thesis: ( A c= M implies {A} is MSSubsetFamily of M )
assume A c= M ; :: thesis: {A} is MSSubsetFamily of M
then A in bool M by MBOOLEAN:18;
then {A} c= bool M by PZFMISC1:33;
hence {A} is MSSubsetFamily of M by PBOOLE:def 18; :: thesis: verum