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

now

let i be set ; :: 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, PBOOLE:def 5;
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:27
.= {A} . i by A2, Def1 ; :: thesis: verum

end;

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