let I be set ; :: thesis: for y, X, x being ManySortedSet of st not I is empty & y in X \ {x} holds
y <> x
let y, X, x be ManySortedSet of ; :: 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 set such that
A3: i in I by A1, XBOOLE_0:def 1;

now

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

end;

hence y <> x ; :: thesis: verum