let I be set ; :: thesis: for x, y, X being ManySortedSet of I st not I is empty & y in X (\) {x} holds
y <> x
let x, y, X be ManySortedSet of I; :: thesis: ( not I is empty & y in X (\) {x} implies y <> x )
assume that
A1: not I is empty and
A2: y in X (\) {x} ; :: thesis: y <> x
consider i being object such that
A3: i in I by A1, XBOOLE_0:def 1;

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

take i = i; :: thesis: y . i <> x . i
y . i in (X (\) {x}) . i by A2, A3;
then y . i in (X . i) \ ({x} . i) by A3, PBOOLE:def 6;
then y . i in (X . i) \ {(x . i)} by A3, Def1;
hence y . i <> x . i by ZFMISC_1:56; :: thesis: verum

end;

hence y <> x ; :: thesis: verum