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 :: thesis: for i being object st i in I holds
A . i = B . i

let i be object ; :: 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;
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 ; :: thesis: verum