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

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

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

end;

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