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

now :: thesis: for i being object st i in I holds
{x} . i = {y} . i

let i be object ; :: thesis: ( i in I implies {x} . i = {y} . i )
assume A2: i in I ; :: thesis: {x} . i = {y} . i
then {x} . i c= {y} . i by A1;
then {(x . i)} c= {y} . i by A2, Def1;
then A3: {(x . i)} c= {(y . i)} by A2, Def1;
thus {x} . i = {(x . i)} by A2, Def1
.= {(y . i)} by A3, ZFMISC_1:18
.= {y} . i by A2, Def1 ; :: thesis: verum

end;

hence {x} = {y} ; :: thesis: verum