let I be set ; :: thesis: for A, M being ManySortedSet of st A c= M holds
{A} is MSSubsetFamily of M
let A, M be ManySortedSet of ; :: 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:19;
then {A} c= bool M by PZFMISC1:36;
hence {A} is MSSubsetFamily of M by PBOOLE:def 23; :: thesis: verum