let I be set ; :: thesis: for x, y being ManySortedSet of st not I is empty & {x} \ {y} = {x} holds
x <> y
let x, y be ManySortedSet of ; :: 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

consider i being set 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 9
.= {(x . i)} by A2, A3, Def1 ;
hence x . i <> y . i by ZFMISC_1:20; :: thesis: verum

end;

hence x <> y ; :: thesis: verum