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

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

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

end;

hence A = B ; :: thesis: verum