let I be set ; :: thesis: for x, y being ManySortedSet of I st not I is empty & {x} (\) {y} = {x} holds
x <> y
let x, y be ManySortedSet of I; :: thesis: ( not I is empty & {x} (\) {y} = {x} implies x <> y )
assume that
A1: not I is empty and
A2: {x} (\) {y} = {x} ; :: thesis: x <> y

now :: thesis: ex i being object st x . i <> y . i

consider i being object such that
A3: i in I by A1, XBOOLE_0:def 1;
take i = i; :: thesis: x . i <> y . i
{(x . i)} \ {(y . i)} = ({x} . i) \ {(y . i)} by A3, Def1
.= ({x} . i) \ ({y} . i) by A3, Def1
.= ({x} (\) {y}) . i by A3, PBOOLE:def 6
.= {(x . i)} by A2, A3, Def1 ;
hence x . i <> y . i by ZFMISC_1:14; :: thesis: verum

end;

hence x <> y ; :: thesis: verum