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

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

let i be object ; :: thesis: ( i in I implies x . i = y . i )
assume A2: i in I ; :: thesis: x . i = y . i
then {(x . i)} /\ {(y . i)} = {(x . i)} /\ ({y} . i) by Def1
.= ({x} . i) /\ ({y} . i) by A2, Def1
.= ({x} (/\) {y}) . i by A2, PBOOLE:def 5
.= {(x . i)} by A1, A2, Def1 ;
hence x . i = y . i by ZFMISC_1:12; :: thesis: verum

end;

hence x = y ; :: thesis: verum