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

now :: thesis: for i being object st i in I holds
x . i = A . i

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

end;

hence x = A ; :: thesis: y = A

now :: thesis: for i being object st i in I holds
y . i = A . i

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

end;

hence y = A ; :: thesis: verum