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

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 . i)} = {x} . i by Def1
.= {(A . i),(B . i)} by A1, A2, Def2 ;
hence x . i = A . i by ZFMISC_1:4; :: thesis: verum

end;

hence x = A ; :: thesis: x = B

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

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

end;

hence x = B ; :: thesis: verum