let I be set ; :: thesis: for A, B being ManySortedSet of I st {A} c= {B} holds
A = B
let A, B be ManySortedSet of I; :: thesis: ( {A} c= {B} implies A = B )
assume A1: {A} c= {B} ; :: thesis: A = B

now

let i be set ; :: thesis: ( i in I implies A . i = B . i )
assume A2: i in I ; :: thesis: A . i = B . i
then {A} . i c= {B} . i by A1, PBOOLE:def 2;
then {A} . i c= {(B . i)} by A2, Def1;
then {(A . i)} c= {(B . i)} by A2, Def1;
hence A . i = B . i by ZFMISC_1:18; :: thesis: verum

end;

hence A = B by PBOOLE:3; :: thesis: verum