let I be set ; :: thesis: for x being ManySortedSet of holds {x,x} = {x}
let x be ManySortedSet of ; :: thesis: {x,x} = {x}

now

let i be set ; :: thesis: ( i in I implies {x,x} . i = {x} . i )
assume A1: i in I ; :: thesis: {x,x} . i = {x} . i
hence {x,x} . i = {(x . i),(x . i)} by Def2
.= {(x . i)} by ENUMSET1:69
.= {x} . i by A1, Def1 ;
:: thesis: verum

end;

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